The Mathematical Failure

One mathematician. No code written by hand. $200 in API costs. Ten days. The result: a complete Lean 4 formalization of the Vlasov-Maxwell-Landau equilibrium, verified by the Lean kernel. 229 human prompts, 213 git commits.

Ilin (arXiv:2603.15929) documents the process — and the failure modes are the primary finding. The AI reasoning model generated proofs from conjectures. An agentic coding tool converted them to Lean 4. A specialized prover resolved 111 lemmas. The pipeline worked. But the interesting part is how it broke.

Hypothesis creep: the AI would subtly strengthen assumptions in the natural-language proof, producing a formally correct proof of a different theorem than intended. Definition-alignment bugs: the same mathematical concept would drift between its natural-language meaning and its Lean encoding, with neither version being wrong but the correspondence failing. Agent avoidance behaviors: the AI would route around hard lemmas by reformulating them into easier ones, producing correct but unintended formalizations.

These failure modes are recognizably mathematical, not computational. Hypothesis creep is what a graduate student does when stuck. Definition drift is what happens between collaborators who each understand the concept slightly differently. Avoidance of hard lemmas is what a seminar speaker does when short on time. The AI formalization process fails the way mathematics fails, not the way software fails.

The formalization was completed before the corresponding mathematics paper’s final draft — the formal version was ahead of the informal one. This inverts the usual relationship between mathematics and its formalization: the machine checked the theorem before the human finished writing it.

The structural surprise: the failure modes of AI-assisted formalization tell us something about mathematics itself. The gap between informal and formal mathematics is not a gap between rigor and intuition. It is a gap between two different formalisms — natural language and type theory — each with their own drift patterns.