{"id":23165,"date":"2026-09-04T12:57:44","date_gmt":"2026-09-04T10:57:44","guid":{"rendered":"https:\/\/djalil.chafai.net\/blog\/?p=23165"},"modified":"2026-09-15T11:32:35","modified_gmt":"2026-09-15T09:32:35","slug":"lean-formalization-with-ai","status":"publish","type":"post","link":"https:\/\/djalil.chafai.net\/blog\/2026\/09\/04\/lean-formalization-with-ai\/","title":{"rendered":"Lean formalization with AI"},"content":{"rendered":"<figure id=\"attachment_23201\" aria-describedby=\"caption-attachment-23201\" style=\"width: 300px\" class=\"wp-caption aligncenter\"><a href=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies.png\"><img loading=\"lazy\" class=\"size-medium wp-image-23201\" src=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies-300x196.png\" alt=\"Lean formal dependency graph\" width=\"300\" height=\"196\" srcset=\"https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies-300x196.png 300w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies-1030x673.png 1030w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies-768x502.png 768w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/theorem_1_9_dependencies.png 1500w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><figcaption id=\"caption-attachment-23201\" class=\"wp-caption-text\">Lean formal dependency graph<\/figcaption><\/figure>\n<p style=\"text-align: justify;\">I have just obtained an automatic Lean formalization of Theorem 1.9 in my most recent paper <a href=\"https:\/\/arxiv.org\/abs\/2608.19358v2\">arXiv:2608.19358v2<\/a>. 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.<\/p>\n<ul>\n<li><a href=\"https:\/\/djalil.chafai.net\/docs\/Lean\/ginibre_poincare_lean_sources_2026-09-04\/documentation.html\">Explore the Lean code online<\/a><\/li>\n<li><a href=\"http:\/\/djalil.chafai.net\/docs\/Lean\/ginibre_poincare_lean_sources_2026-09-04.tar.gz\">Get the Lean code in a single archive<\/a><\/li>\n<\/ul>\n<p style=\"text-align: justify;\">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.<\/p>\n<p style=\"text-align: justify;\"><strong>Quoting Codex.<\/strong><\/p>\n<blockquote style=\"font-size: small;\"><p>\u2022 Completed the full Theorem 1.9 formalization.<\/p>\n<p>Key results:<\/p>\n<p>- Added the unconditional concrete_theoremOneNine.<br \/>\n- Proved the Gaussian \u2202\u0304 coefficient-raising identity.<br \/>\n- Proved the weighted Hermite-energy HasSum.<br \/>\n- Established that the normalized Vandermonde ground state belongs to antiholomorphic degree zero.<br \/>\n- Transferred positive modes from the compact uncentered transform to the centered observable.<br \/>\n- Formalized the Hermite weighted domain and finite-mode form-core approximation.<br \/>\n- Corrected the positive-mode domain weight to k + 1.<br \/>\n- Updated the project status, README, imports, Makefile, and axiom audit.<\/p>\n<p>Verification succeeded:<\/p>\n<p>- Full make completed successfully.<br \/>\n- No sorry, admit, sorryAx, or project axioms were found.<br \/>\n- concrete_theoremOneNine uses only the standard Mathlib axioms propext, Classical.choice, and Quot.sound.<br \/>\n- Only the local Mathlib checkout (ginibre_poincare\/.lake\/packages\/mathlib) was used.<\/p>\n<p>Main theorem: ginibre_poincare\/GinibrePoincare\/Endgame\/ConcreteTheoremOneNine.lean<\/p>\n<p>Total goal usage: 8,067,824 tokens over approximately 5 hours 48 minutes.<\/p><\/blockquote>\n<p style=\"text-align: justify;\"><strong>Note.<\/strong> 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.<\/p>\n<p><a href=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_.webp\"><img loading=\"lazy\" class=\"aligncenter size-medium wp-image-23166\" src=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-300x94.webp\" alt=\"Lean Logo\" width=\"300\" height=\"94\" srcset=\"https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-300x94.webp 300w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-1030x321.webp 1030w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-768x240.webp 768w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-1536x479.webp 1536w, https:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_.webp 1920w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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&#8230;<\/p>\n<div class=\"more-link-wrapper\"><a class=\"more-link\" href=\"https:\/\/djalil.chafai.net\/blog\/2026\/09\/04\/lean-formalization-with-ai\/\">Continue reading<span class=\"screen-reader-text\">Lean formalization with AI<\/span><\/a><\/div>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"iawp_total_views":121},"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165"}],"collection":[{"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/comments?post=23165"}],"version-history":[{"count":55,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions"}],"predecessor-version":[{"id":23315,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions\/23315"}],"wp:attachment":[{"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/media?parent=23165"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/categories?post=23165"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/tags?post=23165"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}