Name the Biggest Number
A Coq-based competition for formally proving the largest constructive number within computational constraints.
Overview
This 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.
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.