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.

翻译：近期研究表明，编码智能体能够使用 Lean 4 形式化整个高等数学教材，但现有工作集中于已在 mathlib 中充分表示的数学分支，且仅通过内核接受程度衡量成功性。我们通过将编码智能体应用于《常微分方程数值方法》的形式化来突破这两项局限——这部数值分析教材在 mathlib 中基本缺失，这考验了智能体从零构建新理论的能力。我们进一步引入系统化、可复现的三维框架，用于评估智能体生成形式化作品的质量（超越编译验证）：语义正确性、Mathlib 复用度及通过 LLM-as-judge 方法实现的跨文件复用度。将该框架应用于自身形式化结果及 RepoProver 与 M2F 公开输出后，我们发现了内核接受完全掩盖的反复出现的不忠实形式化模式，包括不完整的多部分陈述、新增弱化假设及参数限制。研究结果表明，基于编译的指标会实质性高估形式化质量，我们提供了可复现的审计方法论，以支持对自动形式化系统进行更严格的评估。