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. Palomar registration is a separate step.
| 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 |
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.
Note. A large automatic Lean formalization is the one of the Fermat Last Theorem : 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 discrete mathematics are less consuming.
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.