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

arXiv: https://arxiv.org/abs/2606.14000 · HTML: https://mlsanity.com/paper/2606.14000/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 30 references that are in the map.
- First posted on arXiv 12 Jun 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 14 of 14)

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents](https://mlsanity.com/paper/2603.06737/) (2026)

## Built on by (most cited first, 5 of 5)

- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)

## Abstract (arXiv)

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.