{"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-04T15:10:14","modified_gmt":"2026-09-04T13:10:14","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":"<p><a href=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_.webp\"><img loading=\"lazy\" src=\"http:\/\/djalil.chafai.net\/blog\/wp-content\/uploads\/2026\/09\/Lean_logo2.svg_-300x94.webp\" alt=\"Lean Logo\" width=\"300\" height=\"94\" class=\"aligncenter size-medium wp-image-23166\" 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<p style=\"text-align:justify;\">\nI have just obtained a Lean development of Theorem 1.9 in my most recent paper <a href=\"https:\/\/arxiv.org\/abs\/2608.19358v2\">2608.19358v2<\/a>. 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.<\/p>\n<p style=\"text-align:justify;\">Quoting Codex:<\/p>\n<blockquote style=\"font-size:small;\"><p>\n\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.\n<\/p><\/blockquote>\n<p style=\"text-align:justify;\"><strong>Further reading.<\/strong><\/p>\n<ul>\n<li><a href=\"http:\/\/djalil.chafai.net\/docs\/Lean\/ginibre_poincare_lean_sources_2026-09-04\/\">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<li><a href=\"http:\/\/djalil.chafai.net\/docs\/Lean\/ginibre_poincare_lean_sources_2026-09-04\/theorem_1_9_dependencies.svg\">Browse the formal dependency graph<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>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&#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":9},"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":34,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions"}],"predecessor-version":[{"id":23200,"href":"https:\/\/djalil.chafai.net\/blog\/wp-json\/wp\/v2\/posts\/23165\/revisions\/23200"}],"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}]}}