Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess et autres
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 …
0 citations
arXiv (Cornell University)