arXiv:2606.14000 — AI Agent Formalizes a Math Textbook: Compilation Does Not Guarantee Correctness

The Grand Ambition: An Entire Textbook in Lean 4

Formal verification of mathematics — proving theorems in systems such as Lean 4, Coq, or Isabelle — traditionally requires thousands of hours of expert manual work. Researchers Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess, and Vasily Ilin applied an automated agentic pipeline to an ambitious goal: formalize an entire textbook on numerical methods for ordinary differential equations in Lean 4 with the Mathlib library.

Numerical analysis is a particularly demanding target because this branch of mathematics is relatively underrepresented in existing formal libraries — meaning the agent cannot simply invoke already-proven lemmas but must build the formalized foundations from scratch.

Is Compilation Sufficient Proof of Correctness?

The standard metric for evaluating agents that write formal mathematical code is kernel acceptance — does the code pass through the Lean verifier without errors? At first glance, this looks like a solid signal: if the kernel accepts a statement, it is formally proven correct.

The research refutes this assumption. The authors found that kernel acceptance fundamentally conceals semantic errors — agents regularly produce statements that compile but are mathematically incorrect. Moreover, compilation-based metrics substantially overestimate the actual quality of formalization, calling into question the reliability of evaluation protocols that rely exclusively on this signal.

Three Systematic Failure Patterns

The agentic pipeline exhibited three recurring error patterns that compilation does not catch.

Added hypotheses that weaken theorems. The agent formulates a theorem with additional assumptions absent from the original. The statement is technically correct within those assumptions — but proves a weaker claim. For example, a general theorem about the convergence of a numerical method may be restricted to a special case with positive coefficients, which Lean accepts but no researcher would.

Incomplete coverage of multi-part statements. When a theorem has multiple conclusions or cases, the agent may formalize only part of it. Lean accepts this as a valid but partial formalization. Coverage of the original theorem remains incomplete with no diagnostic message from the verifier.

Phantom imports. The agent references Mathlib definitions or lemmas that do not exist or have different exported names. In certain contexts Lean tolerates such imports or resolves them partially, letting the error pass through the kernel and leaving a false impression of validity.

The Three-Dimensional Quality Framework

In response, the authors propose a three-dimensional evaluation framework that surpasses the binary accept/reject approach.

The first dimension is semantic correctness — does the formalized statement match the semantics of the original textbook theorem, regardless of whether it passes the kernel check. The second is Mathlib reuse — does the agent use existing definitions, lemmas, and structure from the Mathlib library, or does it reinvent already-proven claims. The third is cross-file reuse — are definitions consistent across different files in the project, or do inconsistent pairs exist that conceal logical gaps.

All three dimensions are evaluated using an LLM-as-judge approach — automated evaluation that is reproducible and scalable. The framework is designed to be applicable to future agentic formalization systems, not just to this specific pipeline.

Broader Implications for AI Coding Benchmarks

The paper has consequences that reach far beyond formal mathematics. Compilation as the primary success signal is also used in evaluating AI coding agents for standard software — benchmarks such as HumanEval or SWE-bench rely on test passing as a proxy for correctness.

If the same problem exists there as well — agents that pass tests but produce semantically weakened or partially correct implementations — then standard AI coding benchmarks are insufficiently informative signals. This research provides a formal argument for that concern, backed by concrete error patterns catalogued on a real formalization project.

For teams deploying AI agents to write or verify critical code, the key message is clear: compilation checks and test passing are necessary but not sufficient indicators of correctness. Semantic evaluation — however costly and difficult to automate — remains an unavoidable step.