**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.** So far that amounts to roughly **2.5 million lines of machine-checked Lean 4** across a dozen projects — research monographs, textbooks, PDE papers, 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*](https://arxiv.org/abs/2607.13531), arXiv:2607.13531 (2026); presented at DNA 32. * ≈1,050 Lean files / 800,000 lines, six pillars, **0 `sorry`, 0 custom axiom**. Every headline theorem rests on exactly the three Mathlib foundational axioms; the remaining trust footprint (a handful of `native_decide` sites) 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. # The Ramanujan Challenge for AI [Repository](https://github.com/xiangyazi24/Ramanujan_Challenge) · [challenge page](https://www.ramanujanmachine.com/ramanujan-challenge/) · July–August 2026 Ten open problems from the Ramanujan Machine group. Each asks for a proof that a recurrence-generated sequence converges to a named constant (π, *e*, γ, Catalan's *G*, ζ(2), ζ(3), …). * **9 of the 10 problems fully formalized in Lean 4 with 0 `sorry`** (261 files, ≈183k lines); every non-`sorry` theorem depends only on `{propext, Classical.choice, Quot.sound}`. Problem 3.2 (the Apéry GCD conjecture) remains open, with partial results and 3 declared `sorry`s. * Techniques developed per problem: positive adjoint moments with a contracting Miller cone (2.5); Ore factorization / reduction of order (2.6); Barnes contour integrals with gauge transfer (2.7); CM evaluation and period bridge, imported from Ripple (2.8); Bloch–Wigner dilogarithm with rational reconstruction (3.1). # SAIR Foundation — Inverse Galois Problem in degree 24 (IGP24) **Overall rank 9**, score 1,025.5001, team `IGP24-T00171`. Externally verifiable on my SAIR profile: [sair.foundation/u/86340449](https://sair.foundation/u/86340449). The task is to exhibit degree-24 integer polynomials realizing specified transitive groups 24T1–24T25000 — 165,836 (group, real-root-count) pairs, against an LMFDB baseline of 622 — scored on discriminant size and rarity. My entry ran a search pipeline over MAGMA / PARI-GP / SageMath with discriminant-quality scoring and AI-guided coefficient search. # A research PDE trilogy, formalized [Repository](https://github.com/xiangyazi24/Shen_work) 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. 2,137 files / ≈804k lines, 0 `sorry`. # *Proofs from THE BOOK* — all 40 chapters [Repository](https://github.com/xiangyazi24/proof_in_the_book) 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 [Repository](https://github.com/xiangyazi24/invitation-to-qseries-lean) Hei-Chi Chan's book, from the definition of a partition to the tenth-order mock theta identity that closes its hardest chapter. * **255,073 lines across 173 files; 26,504 theorems and lemmas; 1,151 definitions.** An audit module runs **351 `#print axioms` checks**, and every audited theorem depends only on `{propext, Classical.choice, Quot.sound}` — no `sorry`, no custom axiom, no `native_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 [Repository](https://github.com/xiangyazi24/AnalyticCombinatorics) 419 files, ≈129,000 lines, 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.