AI for Mathematics
AI writes. Lean checks.
This page collects the work I began in Spring 2026 on AI-driven formalization. Ordinary AI output may be right, wrong, or hallucinated; the change is that we no longer have to trust the prose, because we ask for a proof in a language Lean can check. AI writes. Lean checks. The projects span research monographs, textbooks, PDE papers, and open competition problems.
A proof enters a library here only after three gates: the statement is faithful to the theorem we intended, the Lean kernel accepts the proof with no placeholders or custom axioms, and a fresh build passes.
Three of these projects turned up errors in published proofs. Formalization at this scale tends to surface that kind of thing, which is a good part of why it is worth doing.
The list below is ordered by what I have been working on most recently, not chronologically.
Ripple — an AI-formalized Lean 4 framework for computing with CRNs
Ho-Lin Chen and Xiang Huang, Ripple: An Open, AI-Formalized Lean 4 Framework for Computing with CRNs, arXiv:2607.13531 (2026); presented at DNA 32.
- Six pillars, 0
sorry, 0 custom axiom. Every headline theorem rests on exactly the three Mathlib foundational axioms; the remaining trust footprint (a handful ofnative_decidesites) is enumerated file-by-file rather than hidden. - Formalizes real-time CRN computability and the full GPAC → dual-rail → large-population-protocol compilation pipeline; three landmark majority protocols (approximate, exact, self-stabilizing exact); three machine-checked versions of Kurtz’s mean-field theorem; and two classical Turing-completeness results (Bournez–Graça–Pouly; Soloveichik–Cook–Winfree–Bruck).
- Repaired real gaps in published proofs — a compilation step that can transiently leave the unit interval, and an algebraic-number construction that silently rested on Catalan’s conjecture — and surfaced a sharp new open problem about when a holonomic series admits an exact, rational-data polynomial-ODE encoding.
Limits of recurrence-generated sequences
Lean 4 formalizations of limits of recurrence-generated sequences converging to classical constants (π, γ, Catalan’s G, ζ(2) + ζ(3), …).
A research PDE trilogy, formalized
A source-faithful Lean 4 formalization of three papers of Wenxian Shen and coauthors on traveling
waves, boundedness and global existence for chemotaxis–logistic systems,
with 0 sorry.
Proofs from THE BOOK — all 40 chapters
Aigner & Ziegler, 6th edition. 40/40 chapters, 0 sorry, 0 axiom. Chapters with substantial
original formalization rather than Mathlib wrappers include Zagier’s one-sentence two-squares proof
(full involution and fixed-point analysis), Monsky’s theorem via Sperner parity, the Herglotz trick,
Galvin’s theorem (the Dinitz conjecture), the five-color Kempe-chain argument, and the Kneser-graph
chromatic number.
An Invitation to q-Series — a complete book formalization
Hei-Chi Chan’s book, from the definition of a partition to the tenth-order mock theta identity that closes its hardest chapter.
- An audit module runs 351
#print axiomschecks, and every audited theorem depends only on{propext, Classical.choice, Quot.sound}— nosorry, no custom axiom, nonative_decide. - Euler’s pentagonal number theorem by two independent routes (Franklin’s involution and formal power series); the Jacobi triple product analytically over ℂ and as a formal Laurent identity; both Rogers–Ramanujan identities via Schur’s 1917 proof; the Rogers–Ramanujan continued fraction and its differential equation through Dobbie’s identity over ℤ[i].
- Ramanujan’s congruences 5 | p(5n+4), 7 | p(7n+5), 11 | p(11n+6) for all n, via a k-section operator over (ℤ/p)⟦X⟧, plus Ono-style infinite families.
Flajolet–Sedgewick, Analytic Combinatorics — all nine chapters
622 audited theorems, 0 sorry / 0 axiom / 0 native_decide.
- The sharp Hardy–Ramanujan partition asymptotic p(n) ∼ exp(π√(2n/3)) / (4n√3), proved unconditionally, without the circle method or modular forms, by an elementary first-entrance renewal route; singularity analysis and saddle-point coefficient machinery carried to third order; Lagrange inversion, Pólya enumeration, the Flajolet continued-fraction theorem, and the multivariate Goncharov–Kolchin limit law.
Useful links
Lean community
- Lean community — documentation, tutorials, and the Zulip chat where Lean users meet.
- Mathlib documentation — reference for the main library of formalized mathematics in Lean 4.
Learning Lean
- Natural Number Game — a gentle, game-style first introduction to writing proofs in Lean.
Platforms
- prove2.me — an open platform of Lean theorem statements and machine-checked proofs.
Formalization service
- Formally Correct — Lean 4 formalization of mathematics and theoretical computer science papers.