Abstract
Recent work has demonstrated that coding agents can formalize entire advanced mathematics textbooks in Lean 4, yet existing efforts concentrate on branches of mathematics already well-represented in mathlib and measure success solely through kernel acceptance. We address both limitations by applying a coding agent to formalize "Numerical Methods for Ordinary Differential Equations," a textbook in numerical analysis that is largely absent from mathlib, stressing the agent's capacity to develop new theory from scratch.
We further introduce a systematic, reproducible three-dimensional framework for evaluating the quality of agent-produced formalizations beyond compilation: semantic correctness, Mathlib reuse, and cross-file reuse via LLM-as-judge methods. Applying this framework to our own formalization and to the released outputs of RepoProver and M2F, we uncover recurring unfaithful formalization patterns, including incomplete multi-part statements, added weakening hypotheses, and parameter restrictions, that kernel acceptance entirely obscures.
Our results suggest that compilation-based metrics substantially overstate formalization quality, and we provide a reproducible audit methodology to support more rigorous evaluation of future autoformalization systems.
Blogger's Review: This research not only pushes the boundaries of mathematical formalization but also introduces a new method for evaluating formalization quality, highlighting the shortcomings of traditional kernel acceptance standards. It holds significant practical implications and theoretical value, laying a solid foundation for the future development of automatic formalization systems.