Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance

This article presents a novel approach to formalizing numerical analysis by applying a coding agent to the textbook "Numerical Methods for Ordinary Differential Equations" in Lean 4, addressing gaps in existing mathematical libraries. It introduces a comprehensive evaluation framework that assesses agent-produced formalizations on semantic correctness, Mathlib reuse, and cross-file reuse, revealing issues in formalization quality that traditional kernel acceptance metrics overlook. This work is significant for practitioners as it offers a reproducible audit methodology, enhancing the rigor of evaluating autoformalization systems in the context of advanced mathematics.