I have just obtained a Lean development of Theorem 1.9 in my most recent paper 2608.19358v2. I did that using the Codex CLI on Debian GNU/Linux, with a ChatGPT Pro account (5.6 Sol). After few manual explorations to select a suitable theorem, I have then asked Codex to use agents for the formalization. It took roughly 6 hours on my desktop computer, 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 Hermite polynomials for complex Gaussians.
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.
Further reading.
Leave a Comment