Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.15929 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915903973621760 |
|---|---|
| author | Ilin, Vasily |
| author_facet | Ilin, Vasily |
| contents | We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code.
The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_15929 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium Ilin, Vasily Artificial Intelligence Analysis of PDEs Logic 68V15 (primary), 68T01, 35Q83, 82D10 (secondary) I.2.3; F.4.1; J.2 We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code. The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished. |
| title | Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium |
| topic | Artificial Intelligence Analysis of PDEs Logic 68V15 (primary), 68T01, 35Q83, 82D10 (secondary) I.2.3; F.4.1; J.2 |
| url | https://arxiv.org/abs/2603.15929 |