For a person like me, intellectually and emotionally, the present fusion between mathematics and computer science is exciting. It also reinforces the fusion between mathematics and theoretical physics, which is exciting as well. It is definitely a strong connection with what mathematicians were two centuries ago, a sort of reunification of the three fundamental forces of structuralism: the hypothetico-deductive force, the natural science force, and the algorithmic force.
I have just conducted the automatic formalization in Lean of all the asserted results of my Ginibre Poincaré paper arXiv:2608.19358v2 using Codex CLI. Coverage concerns the asserted mathematical results, on the domains specified in the mathematical paper. It does not include certification of the numerical experiments or the open research problems. Some results are formalized using multiple proof routes, for instance the nonquadratic radial Ginibre LSI is obtained using both Gaussian contraction and the Bakry-Émery criterion. The full-paper formalization proceeded over roughly a week, following an earlier preliminary experiment, and involved several attempts. The total active computation time was not measured.
The final global Lean code is relatively large because the paper involves functional analysis, classical analysis, linear algebra, basic probability theory, stochastic calculus, complex analysis, and differential geometry, among other types of mathematics. In particular, the formalization encompasses a Bochner-Kodaira commutation-curvature identity, a Hörmander-Berndtsson $\bar{\partial}$ Poincaré inequality, the Bakry-Émery criterion for the logarithmic Sobolev inequality for strongly log-concave measures via Gaussian approximation and contraction, the complex Hermite polynomials, as well as the optimal Gaussian logarithmic Sobolev inequality from the two-point space by tensorization and the binomial central limit theorem.
Most of the formalization was done with Codex CLI, but Leanstral was also used a little bit, out of curiosity, via Vibe CLI. It was crucial to ask Codex explicitly to use agents for the full formalization, to avoid overly small steps. Moreover, it was useful to follow formalization standards such as the ones of Palomar. The full development passes the project build and axiom audits. Theorem 1.1, an optimal Poincaré inequality for Ginibre, including its equality cases, additionally passes Comparator and the three configured kernels.
This automatic formalization experiment, started from the LaTeX source, was partially supervised in the sense that the way to prove certain intermediate statements was suggested to the AI, such as the proof of optimal Gaussian LSI from the two-point space via tensorization and CLT.
Outcome. This automatic formalization experiment has multiple outcomes. First of all it increases the confidence in the stated theorems. Second, it allows to learn new mathematics, selected by the AI as being a short path to formalize given some background knowledge. We have here a link with percolation from the axioms and Mathlib, and also a notion of formalization complexity à la Kolmogorov. A third outcome is the identification of elementary pieces which are sufficiently universal to be potentially included in Mathlib after some rework, such as multivariate/complex Hermite polynomials, or Gaussian Poincaré and log-Sobolev functional inequalities.
Counts. Counts include comments and blank lines. Imported Mathlib modules are counted once in full, these are source-module counts, not the size of a minimal proof-dependency closure:
| Source scope | Files/modules | Physical lines |
|---|---|---|
| Active project Lean sources | 1,727 | 186,672 |
| Transitively imported Mathlib | 3,813 | 1,256,051 |
| Project plus imported Mathlib | 5,540 | 1,442,723 |
The manuscript contains several secondary theorems and proofs. The sole formalization of Theorem 1.9, which is a sum of squares formula for the deficit in Theorem 1.1, takes 16400 lines.
Beyond this formalization experiment, it is interesting to recall that the Lean formalization of the Fermat Last Theorem takes about 13 million lines, more than 5 times the size of Mathlib. The one of the first proof of the $\theta(p_c)=0$ conjecture for bond percolation on $\mathbb{Z}^d$, $d\geq2$, takes "only" 97,574 lines, across 251 Lean files, excluding Mathlib, but the mathematics are different.
Further reading.
- Ginibre Poincaré Lean formalization repository on GitHub
- Ginibre Poincaré paper on arXiv
- Ginibre Poincaré Theorem 1.1 on Palomar, the Registry of Lean-verified mathematics
- Preliminary experiment: automatic formalization of Theorem 1.9 (September 4, 2026)
- Fermat Last Theorem Lean formalization on GitHub and Anthropic announcement
- Critical percolation first Lean proof of $\theta(p_c)=0$ on $\mathbb{Z}^{d\geq2}$ and recent progress.
Notes. My colleague Noé Cuneo pointed out that it is possible to avoid using a laptop/desktop machine for formalization, via the cloud facility of ChatGPT. This is in a way dual, and cheaper for the moment, than setting up a local GPU server with an open-weight model such as Leanstral. Regarding the places for registering or uploading Lean code, in addition to Palomar, there is also TauCeti, Lean Pool, and Merely-true, each with its own policy and philosophy. They form layers between live mathematics and Mathlib in some ways. I have learned the existence of Palomar from my coleague Frederic Marbach, and the existence of the other facilities from Filippo Nuccio.
Abelard. The idea of the link with the Abelard/Bernard-de-Clairvaux medieval controversy came during a cultural visit of the city of Sens, during the "Week-end du DMA 2026" in Burgundy.
Leave a Comment