cs.AIMar 16, 2026
SaveSemi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
Organizations: University of Washington
Abstract
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.
Figures & tables
| Project | Prover | LOC | New thm | New defs | Team | AI role | Logs | Domain |
|---|---|---|---|---|---|---|---|---|
| Gauss [ Math, Inc., 2026 ] | Lean 4 | 181K | ✗ | ✗ | 6+ | sorry elim. | ✗ | Geometry |
| Bayer & David [ Bayer et al., 2025 ] | Isabelle | 20K | ✓ | ✓ | 15 | none | ✗ | Num. theory |
| This work | Lean 4 | 10K | ✓ | ✓ | 1 | all code | ✓ | Math. phys. |
| Numina [ Liu et al., 2026 ] | Lean 4 | 8K | ✓ | ✓ | 13 | collab. | ✗ | Analysis |
| AxiomProver [ Chen et al., 2026b ] | Lean 4 | 4.3K | ✓ | 21 | fully auton. | ✗ | Num. theory | |
| AxiomProver [ Chen et al., 2026c ] | Lean 4 | 2.7K | ✓ | 21 | fully auton. | ✗ | Algebra |
Table 1: Recent research-level formalizations with publicly available code, sorted by LOC. “New thm” = theorem previously unpublished. “New defs” = required definitions or theory not in the proof library ( ✓ = substantial, = lightweight, ✗ = none). “AI role”: sorry elim. = eliminated sorry’s in human-written scaffold; all code = AI generated all proof-assistant code from NL prompts; collab. = human-AI pair programming; fully auton. = AI from NL problem statement alone. “Logs” = full development process public (all commits, prompts, and interaction logs). Discovered an error in the published proof. 22K lines (definitions, statements) written by human experts; Gauss eliminated 160K lines of sorry’s in 3 weeks. No paper; 6+ named contributors on blog post.
Figure 1: ArXiv papers using Lean for formalization, by year. Data from the arXiv metadata snapshot (March 2026), filtered for references to the Lean theorem prover.
Figure 3: Proof dependency graph, generated with LeanBlueprint [ Massot, 2020 ] . All nodes are green (fully proved). The graph flows from primitive definitions ( normSq , eucNorm , landauMatrix ) at the top through intermediate results ( H_theorem , D_zero_implies_maxwellian , the field and conservation lemmas) down to theorem42 and its concrete Coulomb instantiation coulomb_concrete at the bottom. An interactive version is available in the repository.
| Date | Event | Sorry count |
|---|---|---|
| Feb 28 | Gemini generates natural-language proof | – |
| Mar 1 | First Lean code committed (monolithic file) | 25 |
| Mar 2 | First Aristotle submissions; hypothesis creep begins | 25 |
| Mar 3 | File split into main/ directory; Aristotle results arrive | |
| Mar 5 | Concrete torus representation chosen (with Gemini) | |
| Mar 7 | Abstract theorem reaches 0 sorry ’s | 0 |
Table 2: Project timeline and sorry count evolution.
| Metric | Value |
|---|---|
| Lean 4 files | 34 |
| Lines of code | 10,445 |
| Theorems | 39 |
| Lemmas | 186 |
| Definitions | 28 |
| sorry ’s | 0 |
Table 3: Project statistics. The 229 human prompts exclude bare slash commands like /babysit ; all are archived with timestamps. The mathematician estimates 50 hours of active supervision over 10 days.
Figure 4: Sorry count in main/ over time (85 commits). The sawtooth pattern reflects alternating phases of scaffolding (sorry’s accumulate) and proving campaigns (sorry’s eliminated). Key events: peak 25 on Mar 2 (abstract proof chain stated); Aristotle drops count from 25 7 on Mar 3; first 0 sorry’s on Mar 7 (abstract theorem proved); 35 sorry’s on Mar 8 (Coulomb kernel instantiation begun); 35 0 sprint on Mar 9; brief 1 on Mar 10 (non-vacuousness theorem, immediately resolved).
Figure 5: Lean lines of code over time (all 213 commits). The project progressed in four phases: (1) Abstract proof chain (Mar 3 – 6), formalized against an abstract FlatTorus3 typeclass. (2) Coulomb kernel analysis (Mar 7 – 9), handling the singularity at – the sharp LOC increase reflects 4K lines of analytical estimates. (3) Cleanup (Mar 10, early): 3K lines of dead code, redundant lemmas, and unnecessary heartbeat overrides removed. (4) Non-vacuousness (Mar 10, late): satisfiability of the 12 hypotheses.
Figure 6: Claude Code activity across two machines (local university server). Top: messages per hour (red = interactive human, orange = automated, blue = assistant). Bottom: hour-of-day heatmap. The 27,186 assistant turns versus 229 human prompts give a 119:1 ratio, reflecting the high autonomy of each /babysit cycle (typically 20 – 50 tool calls per invocation). The heatmap shows near-round-the-clock activity on Mar 9 – 10 when both machines ran /babysit loops concurrently.
Figure 7: Token consumption across the project. Top: cumulative input tokens (blue, 2.8B) and output tokens (red, 11M). The 254:1 input-to-output ratio reflects the read-heavy nature of formal verification – Claude reads far more context than it writes. Bottom: per-turn context size, showing a sawtooth pattern as the context window fills to 175K tokens and resets at each of the 164 autocompacts (red vertical lines). Dense compaction clusters on Mar 6 – 10 correspond to the intensive Coulomb kernel analysis and /babysit loop periods.
Figure 8: Tool usage across 17,334 invocations. Left: totals by category. The core editing loop dominates – Bash (3,975), Read (3,416), Edit (2,495), Grep (1,701), Write (900) – reflecting the iterative nature of formal verification. Lean LSP tools (3,194 combined) provided real-time feedback. Right: daily breakdown showing the ramp-up from exploratory work (Feb 28 – Mar 2) through peak activity (Mar 6 – 10) when both machines ran /babysit loops concurrently.
Figure 9: Outcomes of 220 Aristotle submissions. Aristotle proved 111 lemmas cleanly (50%), disproved 28 false statements (13%), returned 66 with sorry’s still present (30%), and 15 failed or were never started (7%). The disproved statements were particularly valuable – they caught false conjectures early (e.g., missing measurability hypotheses, Vitali-set counterexamples, incorrect Schwartz decay estimates for the Coulomb kernel). The stacked bar chart shows peak submission activity on Mar 2 (57 jobs) and Mar 6 (45 jobs).
Figure 10: Aristotle turnaround times for 214 submissions, colored by outcome. Left: histogram. Proved lemmas (green) cluster in the first bins (median 9 minutes), while “returned with sorry” (red) dominates the long tail. Right: median turnaround by category. The overall median was 19 minutes. Disproved statements took 29 minutes (counterexample construction); submissions returned with sorry took a median of 5.6 hours – Aristotle exhausts its time budget before giving up.
Figure 11: LOC by file group over time. Red shades are the mathematical proof chain (Sections 2–8, Theorem42 , VMLInputDerive , CoulombConcreteTheorem42 ); blue shades are supporting infrastructure (definitions, torus instance, Coulomb kernel integrability files, decay helpers). At completion, infrastructure accounts for roughly half of the codebase – reflecting the substantial gap between Mathlib ’s current coverage and the background material needed for research-level mathematical physics. The sharp blue growth on Mar 7–8 is the Coulomb kernel analysis ( 4K lines of analytical estimates for the singularity at ). The cleanup phase (Mar 10) primarily removed blue infrastructure code, while the red proof chain remained stable.
Figure 12: Lines of Lean code added and deleted per day. Most days are net-positive (new content), with two exceptions: Mar 3 (monolithic file split into main/ – same code reorganized) and Mar 9 – 10 (cleanup phase removed 3K lines of dead code, redundant lemmas, and unnecessary heartbeat overrides). Total: 21,783 added, 13,478 deleted, net 8,305 lines.