Mini-Rubik
A certified solver for the 2x2 Rubik's Cube, formally verified in Coq.
Overview
Solving the mini Rubik (2x2) in Coq
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.