Starred repositories
12
stars
written in Rocq Prover
Clear filter
Mathematical Components compliant Analysis Library
Formal proof of the Four Color Theorem [maintainer=@ybertot]
A formalization of geometry in Coq based on Tarski's axiom system
A Verified Compiler for Gallina, Written in Gallina
A library of mechanised undecidability proofs in the Coq proof assistant.
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
The formal proof of the Odd Order Theorem
A Verified Implementation of Dijkstra's Algorithm
Formal proof in Coq of Cauchy Schwarz Inequality