{"id":23405,"date":"2026-10-07T22:04:49","date_gmt":"2026-10-07T20:04:49","guid":{"rendered":"https:\/\/djalil.chafai.net\/blog\/?p=23405"},"modified":"2026-10-07T22:31:38","modified_gmt":"2026-10-07T20:31:38","slug":"automatic-formalization-of-a-full-paper-in-lean","status":"publish","type":"post","link":"https:\/\/djalil.chafai.net\/blog\/2026\/10\/07\/automatic-formalization-of-a-full-paper-in-lean\/","title":{"rendered":"Automatic formalization of a full paper in Lean"},"content":{"rendered":"
\"Lean<\/a>
Lean formal dependency graph<\/figcaption><\/figure>\n

I have just conducted the automatic formalization in Lean of all my Ginibre Poincar\u00e9 paper arXiv:2608.19358v2<\/a> 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 a separate formalization of every alternative proof. It took hours and the Lean code is relatively big in total because the paper involves functional analysis, stochastic calculus, and complex analysis, among other things. In particular, the formalization encompasses complex Hermite polynomials as well as the optimal Gaussian logarithmic Sobolev inequality, proved from the two-point space by tensorization and the binomial central limit theorem. Most of the formalization was done with Codex CLI, but I have also played successfully with Leanstral. What is really important is to ask Codex explicitly to use agents for the full formalization, and to use the standards of Palomar. The full development passes the project build and axiom audits. Theorem 1.1, including its equality classification, additionally passes Comparator and the three configured kernels. Palomar registration is a separate step.<\/p>\n\n\n\n\n\n
Source scope<\/th>\nFiles\/modules<\/th>\nPhysical lines<\/th>\n<\/tr>\n
Active project Lean sources, including roots and generated facades<\/td>\n1,315<\/td>\n142,364<\/td>\n<\/tr>\n
Transitively imported Mathlib<\/td>\n3,794<\/td>\n1,251,826<\/td>\n<\/tr>\n
Project plus imported Mathlib<\/td>\n5,109<\/td>\n1,394,190<\/td>\n<\/tr>\n<\/table>\n

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.<\/p>\n

Note.<\/strong> 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. It seems that the automatic formalization of the $\\theta(p_c)=0$ conjecture for bond percolation on $\\mathbb{Z}^d$, $d\\geq2$, takes \"only\" about 100,000 lines.<\/p>\n

\"Lean<\/a><\/p>\n

Further reading.<\/strong><\/p>\n