Search papers, labs, and topics across Lattice.
This paper presents a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, showcasing an AI-assisted mathematical research loop. The loop involved using Gemini DeepThink for proof generation, Claude Code for Lean translation, and Aristotle for lemma proving, all supervised by a mathematician. The formalization was completed in 10 days for $200, highlighting the potential for AI to accelerate and reduce the cost of formal mathematical verification.
AI can now semi-autonomously formalize complex mathematical theorems like the Vlasov-Maxwell-Landau equilibrium, even outpacing traditional mathematical research.
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.
