Top Repositories
Formal proof in Coq of Banach-Tarski paradox.
Real Numbers using LPO
Rogue written in OCaml
Formal proof in Coq of Cauchy Schwarz Inequality
Formal proof in Coq of Puiseux's Theorem.
Rocq library defining trigonometry where angles are pairs (x, y) such that x²+y²=1
Repositories
15Rocq library defining common structure for semirings, rings and fields.
Rocq library defining trigonometry where angles are pairs (x, y) such that x²+y²=1
Sensitivity Conjecture in Coq
Formal proof in Coq of Banach-Tarski paradox.
Coq proof of the Euler product formula for the Riemann zeta function (in progress...)
Formal proof in Coq of Cauchy Schwarz Inequality
Formal proof in Coq of Puiseux's Theorem.
Real Numbers using LPO
Homologic Algebra in Coq
Rogue written in OCaml
Experiments with HOTT. Trying to implement it in Coq.
Statement of theorems proven in Coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
No description provided.