{"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-30T14:03:39","modified_gmt":"2026-09-30T12:03:39","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>Leanstral.<\/strong> Instead of using the expensive ChatGPT, it is possible to use the open source (open weights) software Leanstral, available with zeroconf through the CLI Mistral Vibe, the Mistral analogue of Codex! You can download it from HuggingFace.<\/p>\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":207},"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":62,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions"}],"predecessor-version":[{"id":23388,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions\/23388"}],"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}]}}