I have 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 16000 lines of Lean (~75 files). This modest experience suggests to contribute to mathlib, such as for multivariate Hermite polynomials for complex Gaussians.
Quoting Codex:
Theorem 1.9 is fully formalized in Lean as:
concrete_theoremOneNine (ginibre_poincare/GinibrePoincare/Endgame/ConcreteTheoremOneNine.lean)
It proves both exact sum-of-squares identities for the explicitly defined Ginibre
measure and generator on IsTheoremOneNineCore, the collision-free smooth compact
symmetric core. The required Hermite basis, Parseval/lowering theory, weighted-series
convergence, zero-mode geometry, and finite-mode domain approximation are proved
rather than assumed.The full build and axiom audit pass, with no sorry, admit, custom axioms, or theorem-valued
certificates. The only reported dependencies are standard Mathlib foundations: propext,
Classical.choice, and Quot.sound.One scope qualification: it does not claim an additional unspecified self-adjoint extension
beyond the explicit core and weighted form domain. Within the stated formalized scope,
Theorem 1.9 is complete.
Further reading.