I have just obtained an automatic Lean formalization of Theorem 1.9 in my most recent paper arXiv:2608.19358v2. I did that using the ChatGPT Codex CLI on Debian GNU/Linux. After few manual explorations to select the most suitable theorem, I have then asked Codex to use agents for the formalization. It took roughly 6 hours on my desktop workstation, used approximately 8 millions tokens, and produced about 16400 lines of Lean (~75 files). This modest experience suggests to contribute to Mathlib, such as for multivariate complex Hermite polynomials.
The problem with automatic formalization is that the human has to check that what is formalized is really what he wants. This is doable for a small project like this one, which corresponds to a one page proof in the paper. But for more substantial projects, this problem becomes more serious.
Quoting Codex.
• Completed the full Theorem 1.9 formalization.
Key results:
- Added the unconditional concrete_theoremOneNine.
- Proved the Gaussian ∂̄ coefficient-raising identity.
- Proved the weighted Hermite-energy HasSum.
- Established that the normalized Vandermonde ground state belongs to antiholomorphic degree zero.
- Transferred positive modes from the compact uncentered transform to the centered observable.
- Formalized the Hermite weighted domain and finite-mode form-core approximation.
- Corrected the positive-mode domain weight to k + 1.
- Updated the project status, README, imports, Makefile, and axiom audit.Verification succeeded:
- Full make completed successfully.
- No sorry, admit, sorryAx, or project axioms were found.
- concrete_theoremOneNine uses only the standard Mathlib axioms propext, Classical.choice, and Quot.sound.
- Only the local Mathlib checkout (ginibre_poincare/.lake/packages/mathlib) was used.Main theorem: ginibre_poincare/GinibrePoincare/Endgame/ConcreteTheoremOneNine.lean
Total goal usage: 8,067,824 tokens over approximately 5 hours 48 minutes.
Note. The largest formalization ever, obtained using AI, is the Lean proof of the Fermat Last Theorem : about 13 millions lines, more than 5 times the size of Mathlib.
