Sudoku
A certified Sudoku solver implemented in Coq using a formalized Davis-Putnam procedure.
Overview
A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
Related Projects
Name the Biggest NumberThis repository hosts a formal competition where participants submit constructive numbers defined in Coq, along with proofs that each new number exceeds the previous contender. It applies rigorous computational constraints to ensure definitions are verifiable and meaningful within recreational mathematics. ## Key Features - **Formal Verification** — All numbers and their comparisons must be formally specified and proven in Coq. - **Constructive Numbers** — Only computable numbers are allowed, excluding non-constructive concepts like Busy Beaver numbers. - **Computational Constraints** — Definitions must type-check within 15 seconds, and proofs within 1 minute, on reasonable hardware. - **Structured Submissions** — Participants submit via pull requests following a standardized format in `Contender.v`. - **No Axioms** — Proofs must avoid axioms, using only widely accepted Coq libraries. ## Philosophy The project emphasizes formal rigor and computational feasibility, turning the playful challenge of naming large numbers into a disciplined exercise in proof verification and constructive mathematics.
HanoiHanoi tower in Coq
CoqobanSokoban (in Coq) [maintainer=@erikmd]
T2048a version of the 2048 game for Coq
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.