2 papers
cs.AI2026
Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
Theodore Meek, Siyuan Ge, Di Qiu Xiang +2
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 w…
cs.LG2026
Learning to Repair Lean Proofs from Compiler Feedback
Evan Wang, Simon Chess, Daniel Lee +4
As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively…