Sensitivity Conjecture in Rocq
Proved by Hao Huang
Work in progress... (30 Apr 2025)
sensibility: files for the proof
rngl_alg: examples of algebras of the theory RingLike
Daniel de Rauglaudre
$ rocq -v
The Rocq Prover, version 9.0.0
compiled with OCaml 4.14.1
To compile this project, we must install the opam packages RingLike and TrigoWithoutPi, by type:
opam pin add rocq-ring-like https://github.com/roglo/rocq_ring_like.git
opam pin add rocq-trigo-without-pi https://github.com/roglo/rocq_trigo_without_pi.git