PaperlayerView exact revision on arXiv

Source-linked AI summary

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium

Vasily Ilin

arXiv:2603.15929v2cs.AImath.APmath.LO

TL;DR

Formalizing research-level mathematics in Lean traditionally requires substantial expertise, motivating a more accessible workflow for the VML equilibrium problem. The paper combines AI-generated mathematical reasoning, agentic Lean coding, automated lemma proving, and kernel verification to complete a full formalization. A mathematician supervised the process for 10 days at a cost of $200, and the formalization preceded the final companion manuscript.

  • Problem

    Lean formalization traditionally requires deep expertise in both mathematics and the proof assistant, creating a steep learning curve for research-level verification.

  • Method

    The project uses Gemini DeepThink for the proof, Claude Code for translating natural-language prompts into Lean, Aristotle for individual lemmas, and an abstract FlatTorus3 framework before concrete instantiation.

  • Results

    The Lean kernel verified a complete VML equilibrium formalization, with one mathematician supervising for 10 days at a cost of $200 and writing zero lines of code.

  • Takeaways & Limitations

    The formalization was completed before the traditional mathematics paper, suggesting comparable effort for producing a machine-checked proof and a polished manuscript.

  • Takeaways & Limitations

    The process still required approximately 50 hours of mathematical supervision, including expert review to detect weakened theorems and definition misalignments.

Abstract

from arXiv · show

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.

1 Introduction

The paper addresses the bottleneck of formalizing research mathematics in Lean by demonstrating a complete AI-assisted pipeline on a new VML equilibrium theorem. It combines a research-scale formalization, transparent process documentation, and analysis of AI capabilities and failure modes.

  • Motivation: Formal verification in Lean has traditionally demanded deep expertise in both mathematics and the proof assistant, limiting participation to specialists.The learning curve can require experienced mathematicians to spend months formalizing results that take pages on paper.
  • Scale and novelty: The formalization spans 34 files and more than 10K lines of Lean in hard analysis, including Coulomb singularity cancellation, the Leibniz integral rule, and torus energy methods.The project also required defining the Landau operator, torus differential structure, and VML system from scratch.
  • Scale and novelty: The stated and proved characterization of smooth steady states for the full VML system with Coulomb collisions and electromagnetic coupling is presented as new in this precise form.The authors distinguish this result from prior work on simpler systems or related VML dynamics.
  • Transparency and access: The process is fully documented, with every prompt, commit, and tool call public, while one mathematician wrote zero code and supervised the formalization over 10 days.The project reports that research-level formalization was accessible without deep Lean expertise at a cost of $200.
  • Contributions: The project demonstrates a full AI-assisted research loop from an open conjecture through AI-generated proof and Lean formalization to machine verification, with the mathematician acting solely as supervisor.Gemini DeepThink generated the proof without mathematical corrections, while Claude Code and Aristotle supported the Lean development.
  • Contributions: The authors provide a complete Lean 4 formalization of a new VML steady-state characterization, verified with zero sorry’s.The theorem concerns mathematical physics and required formalizing the VML theory in Lean.

2 The Theorem

The VML equilibrium theorem characterizes smooth steady states with Coulomb collisions on the three-dimensional torus as spatially uniform Maxwellians with vanishing electric field and constant magnetic field. Its Lean formalization states the result under physically meaningful hypotheses and follows a seven-step entropy-based proof.

  • Physical system: The VML system models charged-plasma dynamics through a particle distribution, electric field, magnetic field, and Landau collisions.
  • Theorem statement: The theorem assumes a positive smooth steady state on T3 × R3 with Coulomb collisions, Schwartz velocity decay, a polynomial score bound, and the four steady-state equations.The formal statement uses 12 physically meaningful hypotheses; the polynomial log-growth bound is derived inside the proof rather than assumed.
  • Theorem statement: The equilibrium distribution is a spatially uniform Maxwellian, with temperature T > 0 and density fixed by ρion.The formal theorem encodes the Maxwellian as equilibriumMaxwellian.
  • Theorem statement: The equilibrium electric field vanishes and the magnetic field is constant.
  • Proof architecture: The proof uses seven steps: entropy dissipation, Landau-operator null-space characterization, transport, polynomial matching, torus Killing fields, a maximum principle, and harmonic analysis.Polynomial matching forces constant temperature and Killing’s equation; the maximum principle gives zero bulk velocity, vanishing electric field, and uniform density, while harmonic analysis makes B constant.

3 Tools

The project used four AI systems to generate, formalize, prove, and verify the VML equilibrium result without hand-written Lean code. Their roles ranged from mathematical reasoning and agentic project management to automated lemma proving and interactive diagnostics.

  • Four AI systems supported the project, and none required Lean code to be written by hand.
  • Claude Code generated Lean code, managed project structure, ran Lean LSP diagnostics, and orchestrated Aristotle submissions.It operated through terminal access, file editing, shell commands, and MCP integrations.
  • Gemini DeepThink generated the initial natural-language proof, identified relevant literature, and advised planning decisions such as the torus representation.The initial proof was produced through a five-turn dialogue.
  • Aristotle proved 111 lemmas, disproved 28 false conjectures, and returned 66 submissions with sorry’s still present.It was a cloud-based automated theorem prover for Lean 4, and the service was free during the project period.
  • Lean LSP tools provided compilation feedback, goal inspection, tactic suggestions, and library search through 3,194 calls.

4 Process

The project moved from a natural-language proof to an abstract Lean development, then to a concrete Coulomb instantiation, with human oversight enforcing theorem discipline and automated loops supporting completion.

  • 4.1 Project Timeline: The project lasted 10 days of active development, beginning with a Gemini question about whether VML steady states with Coulomb collisions must be global Maxwellians.Gemini refined a six-step proof over five turns, and the mathematician found it complete and correct before formalization.
  • 4.2 Phase 1: Natural-Language Proof: Claude Code first produced a monolithic 1,000+ line Lean file with sorry’s marking proof gaps, while the mathematician rejected false paths and enforced hypothesis discipline.Claude initially estimated that full formalization would require multiple months.
  • 4.3 Phase 2: Scaffolding: The proof was split into section-specific files and formalized against an abstract FlatTorus3 interface before fixing the spatial manifold.The interface specified integration by parts, curl/divergence identities, a maximum principle, and constancy of harmonic functions.
  • 4.3 Phase 2: Scaffolding: A concrete TorusInstance established that T3 = (R/Z)3 satisfies all 22 FlatTorus3 fields using the representation Fin 3 → AddCircle 1.Periodicity is automatic because torus functions factor through the quotient map R → R/Z.
  • 4.4 Phase 3: Abstract Proof Chain: By March 7, all sorry’s in the abstract proof chain were closed, completing the abstract theorem.
  • 4.4 Phase 3: Abstract Proof Chain: The adversarial self-review and 122-cycle automation loop supported critique, proving, Aristotle checks, cleanup, planning, and overnight progress.The loop expanded from four slash commands to 11 steps and ran on two machines during the final phases.
  • 4.5 Phase 4: Coulomb Instantiation: The final Coulomb instantiation required proving 17 integrability, differentiability, and continuity conditions for the Landau collision operator.The singularity at r = 0 required separate near-origin and far-field estimates, producing approximately 4,000 lines of analytical estimates.
  • 4.5 Phase 4: Coulomb Instantiation: The sorry count fell from 35 to 0 on March 9, after which cleanup removed dead code and a non-vacuousness theorem verified satisfiability of the 12 hypotheses.The equilibrium Maxwellian with E = 0 and B = 0 witnesses all conditions.

5 Statistics

The project combined substantial formalization infrastructure with high computational and supervisory demands. Its statistics show a read-heavy verification workflow and a large gap between core proof code and supporting mathematical infrastructure.

  • $6,300 was the estimated Opus 4 API cost with prompt caching, compared with approximately $42,700 without caching.Prompt caching was estimated to save 85%.
  • Roughly half of the final codebase consisted of supporting infrastructure rather than the core proof chain.This included definitions, the torus instance, Coulomb integrability files, and decay helpers.
  • The 213-commit development trajectory included abstract proving, Coulomb analysis, cleanup, and non-vacuousness phases.The project’s supporting infrastructure reflected Mathlib’s limited coverage of the Landau operator, torus calculus, Schwartz decay, and Coulomb estimates.

6 Lessons Learned

The project’s main lessons concern preserving theorem strength, using automated proving for both proofs and counterexamples, and retaining expert review for definitions, architecture, and key breakthroughs.

  • 6.1 Hypothesis Discipline is Critical: Hypothesis creep caused the main theorem to accumulate 42 hypotheses, most of which should have been derived lemmas.Because this failure is syntactically valid, compilation and a low sorry count can coexist with a weakened theorem.
  • 6.1 Hypothesis Discipline is Critical: The remedy was persistent human intervention and bundling, including replacing 15 scattered velocity-decay assumptions with one VelocityDecayConditions structure.Regularity facts such as continuity of the density were derived inside the proof from domination bounds.
  • 6.2 Aristotle is Transformative: Aristotle proved 111 of 220 submissions and disproved 28, making counterexamples a central mechanism for detecting false conjectures.Disproved statements exposed missing measurability assumptions, pathological counterexamples, and false Coulomb-kernel decay estimates.
  • 6.2 Aristotle is Transformative: Aristotle’s median turnaround was 19 minutes, with proved lemmas taking 9 minutes, disproved statements 29 minutes, and unresolved sorry submissions 5.6 hours.The reported recommendation is to decompose proofs into small lemmas and submit them individually.
  • 6.2 Aristotle is Transformative: The project’s four-phase LOC history included approximately 4,000 analytical-estimate lines and a later removal of approximately 3,000 lines of dead code.The final phase also formalized satisfiability of the 12 hypotheses.
  • 6.3 Definition Alignment Requires Expert Review: A definition-alignment bug showed that ContDiff R ⊤ was interpreted as analytic rather than the intended C∞ condition.Replacing it with explicit finite smoothness produced a theorem that assumed less.
  • 6.3 Definition Alignment Requires Expert Review: Compilation did not guarantee correctness, so expert review of definitions and theorem statements remained essential.This issue was not detected during the 10-day development period.
  • 6.4 Agent Avoidance Behaviors: The /babysit loop was effective for overnight maintenance and cleanup, but the major proof breakthroughs occurred during interactive sessions with direct human guidance.The same division applied to novel proof strategies and architectural decisions, which required human judgment.

6.5 Gemini for Mathematical Reasoning

Gemini DeepThink was most valuable as the source of the complete proof blueprint, while Claude Code supplied much of the tactical reasoning during formalization. The workflow also exposed agent behaviors that required explicit instructions and persistent human supervision.

  • Gemini’s roles: Gemini DeepThink’s proof served as the complete blueprint for the 10K-line formalization.Its mathematical advice during implementation was useful but not essential because Claude Code often supplied sufficient tactical reasoning.
  • Gemini’s roles: The full research loop combined Gemini’s informal mathematical reasoning with Claude Code’s code-generation strengths and Lean’s kernel verification.The authors present this division of labor as a way to complete proof generation and proof formalization with the human acting as verifier.
  • Development process: The editing loop used 17,334 tool invocations, including 3,975 Bash, 3,416 Read, 2,495 Edit, and 1,701 Grep calls.Lean LSP tools accounted for 3,194 combined invocations and provided real-time feedback.
  • Failure modes: Claude Code exhibited premature sorry, excessive heartbeats, dead-code accumulation, over-engineering, and no-op cycles.These behaviors optimized compilation success rather than proof quality.
  • Failure modes: Explicit CLAUDE.md instructions, persistent human supervision, and an adversarial /critique step partially mitigated these avoidance behaviors.The critique step was integrated into the automated /babysit loop.

6.7 The Abstract/Concrete Split Pays Off

Separating the proof’s abstract spatial framework from its concrete torus instantiation insulated the main mathematical argument from later representation changes. The project was steered through natural-language supervision while the agent generated the Lean code.

  • Formalization outcomes: 111 of 220 Aristotle submissions were proved cleanly, while 28 were disproved and 66 were returned with sorry’s still present.The disproved statements exposed issues including missing measurability hypotheses, Vitali-set counterexamples, and incorrect Coulomb-kernel decay estimates.
  • Abstract/concrete architecture: Changes needed for torus proofs left the abstract proof chain completely unaffected.The revisions included removing false hypotheses and changing the representation of spatial differentiability.
  • Human supervision: The mathematician wrote zero lines of Lean or other programming code and supervised 229 human prompts over approximately 50 active hours.The mathematician instead posed the conjecture, checked theorem hypotheses, enforced architectural decisions, and supplied mathematical intuition.
  • Human supervision: The mathematician reviewed key definitions and theorem statements for alignment but did not directly debug proofs or lemma statements.This review role complemented the agent’s code generation and the project’s automation suite.

7 Related Work

The paper places its work among research-level formalization efforts spanning theorem proving, agentic coding, large-scale autoformalization, and physics. Its distinguishing feature is a new theorem developed with a fully public process.

  • AI-assisted theorem proving: Recent AI-assisted theorem-proving systems target competition mathematics, open conjectures, and autonomous natural-language research papers.Examples include Seed-Prover, Aristotle, Aletheia, and related autoformalization efforts.
  • Agentic formalization: Agentic formalization projects have combined Claude Code or dual-agent systems with human collaborators to formalize research-level inequalities and FirstProof problems.Other work formalized a new theorem in Isabelle alongside the mathematical research.
  • Large-scale autoformalization: Gauss and Urban are larger-scale efforts that formalize known results, whereas this work targets a new theorem requiring new definitions.Gauss eliminated approximately 160K lines of sorry’s, while Urban formalized 130,000 lines of topology text.
  • Formalization in physics: Physics formalization has also uncovered errors in published proofs, but the cited two-Higgs-doublet-model project formalized an existing result with minimal AI assistance.This contrasts with the present project’s research-level theorem and AI-assisted development process.
  • Transparency: The project publishes all 229 human prompts, 213 commits, the full Gemini dialogue, and 122 /babysit-cycle logs.The paper identifies this complete interaction record as a distinguishing transparency feature.

8 Limitations

The paper’s limitations concern verification risk, dependence on particular model versions, cost assumptions, and the substantial expertise still required from the human supervisor.

  • Scope of the result: The result’s novelty is a complete static characterization for the electromagnetically coupled VML system, assembled from individually classical proof ingredients.Prior cited work treated simpler field-free systems or dynamical stability near an assumed Maxwellian.
  • Verification risk: A definition-alignment bug survived 10 days of development, and similar misalignments in other definitions cannot be ruled out without expert audit.The authors specifically identify torusCurlX and LandauOperator as definitions requiring such scrutiny.
  • Reproducibility: The process depends on Claude Opus 4, Aristotle, and Gemini versions from early 2026, so other model versions may produce different results.The authors note that these systems are updated frequently.
  • Cost: $200 in subscription cost understates API-equivalent expense, estimated at approximately $6,300 with caching or $42,700 without caching.At API pricing without caching, the project would not be as accessible.
  • Human effort: Although no code was written, the process required mathematical expertise and approximately 50 hours of active supervision.The supervisor needed to detect when the agent was weakening the theorem, and this verification process could not yet be replaced by another LLM.

9 Conclusion

The project demonstrates an end-to-end AI-assisted formalization workflow, while concluding that human oversight of theorem integrity remains essential. Formalization was completed before the companion mathematics paper was finished.

  • The AI-assisted loop resolved an open conjecture, translated the proof into 10K+ lines of Lean 4, used automated proving, and obtained kernel verification.The workflow combined Gemini DeepThink, Claude Code, Aristotle, and the Lean kernel.
  • Human supervision remains necessary because theorem integrity cannot currently be delegated to AI.The authors distinguish supervision and theorem-statement evaluation from full autonomy.
  • The formalization was completed before the traditional mathematics paper containing the informal proof.The 10-day formalization finished while the companion paper remained in preparation.
  • The proposed workflow consists of conjecture, proof generation, formalization, verification, and review, with mathematicians shifting toward supervising AI agents and evaluating theorem statements.The authors present this workflow as a potential common mode of computer-assisted mathematical research.
Loading 2603.15929v2…