Lean 4 formalization projects produced with the
LeanFlow workflow. The main
branch is reserved for projects that are ready to present publicly: each listed
project builds and has no project-local sorry, admit, custom axiom, or
unsafe in its Lean files.
Work-in-progress formalizations are kept on separate draft pull requests instead
of living on main.
- License: Apache License 2.0
- Contribution guide: CONTRIBUTING.md
- Publication notes and limitations: PUBLICATION_LIMITATIONS.md
- Citation metadata: CITATION.cff
- Lake target:
IMO2026 - Source: Joseph Myers,
jsm28/IMOLean, based on the official IMO 2026 problems - Status: proof-complete LeanFlow formalizations of Problems 1–6, produced with
gpt-5.6-solatxhighreasoning effort through the Codex provider and verified together as one Lean project. - Provenance and compact run evidence:
IMO2026/GPT5.6/README.md
- Lake target:
Pyth - Source: Sophie Frisch and Leonid Vaserstein, Parametrization of Pythagorean triples by a single triple of polynomials
- Status: proof-complete source-backed formalization of the obstruction theorem, the integer-valued parametrization, and the positive/16-parameter variants.
- Lake target:
CramerWoldTheorem - Source: Russell Lyons and Kevin Zumbrun, A Calculus Proof of the Cramer-Wold Theorem
- Status: proof-complete source-backed formalization of the half-space theorem, average-distance reconstruction, odd-dimensional inversion, and even-to-odd reduction.
The unfinished formalizations are maintained as draft PR branches:
AShortProofOfTheHiltonMilnerTheorem: A short proof of the Hilton-Milner Theorem, with remaining proof obligations.QuantizingPythagoreanTriples: Quantizing Pythagorean triples, with remaining proof obligations and the source-stated open unimodality conjecture.
Run all completed project builds:
./scripts/check-projects.shOr build an individual project from its directory:
cd PythagoreanPolynomialParametrization
lake build Pyth
cd ../CramerWoldTheorem
lake build CramerWoldTheorem
cd ../IMO2026/GPT5.6
lake build IMO2026