Paper-Level Autoformalizations

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.

Repository Metadata

• License: Apache License 2.0
• Contribution guide: CONTRIBUTING.md
• Publication notes and limitations: PUBLICATION_LIMITATIONS.md
• Citation metadata: CITATION.cff

Completed Projects

IMO2026/GPT5.6

• 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-sol at xhigh reasoning effort through the Codex provider and verified together as one Lean project.
• Provenance and compact run evidence: IMO2026/GPT5.6/README.md

LeanIMOBench/GPT6-astra

• Lake target: LeanIMOBench
• Source: IMO-LeanProofBench, the Lean half of IMO-Bench (Luong et al., Towards Robust Mathematical Reasoning), published as imobench/lean_proof_bench_v2.csv in google-deepmind/superhuman
• Status: proof-complete formalizations of the eighteen benchmark problems that LEAP (arXiv:2606.03303) does not publish solutions for — twelve Geometry and six Combinatorics, twelve of them problems composed for the benchmark and never published. Produced with LeanFlow with gpt-6-astra (xhigh reasoning orchestrator, low reasoning prover) through the Codex provider, and verified together as one Lean project. Every statement is byte-identical to the published benchmark. Proof graphs are in LeanIMOBench/GPT6-astra/DAGS.md.

PythagoreanPolynomialParametrization

• 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.

CramerWoldTheorem

• 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.

Work in Progress

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.

Checks

Run all completed project builds:

./scripts/check-projects.sh

Or build an individual project from its directory:

cd PythagoreanPolynomialParametrization
lake build Pyth

cd ../CramerWoldTheorem
lake build CramerWoldTheorem

cd ../IMO2026/GPT5.6
lake build IMO2026