Pinned Loading

1. rocq_ring_like rocq_ring_like Public

   Rocq library defining common structure for semirings, rings and fields.

   Rocq Prover 1

2. banach_tarski banach_tarski Public

   Formal proof in Coq of Banach-Tarski paradox.

   Coq 16 1

3. puiseuxth puiseuxth Public

   Formal proof in Coq of Puiseux's Theorem.

   Coq 4

4. rocq_trigo_without_pi rocq_trigo_without_pi Public

   Rocq library defining trigonometry where angles are pairs (x, y) such that x²+y²=1

   Rocq Prover 2

5. coq_sensitivity coq_sensitivity Public

   Sensitivity Conjecture in Coq

   Rocq Prover 1

6. coq_euler_prod_form coq_euler_prod_form Public

   Coq proof of the Euler product formula for the Riemann zeta function (in progress...)

   Coq 1