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.

Stars67

Forks7

Last commit3 years ago