2 papers
cs.LG2026
Learned Interventions in Lean 4 grind
Evan Wang, Simon Chess, Sophie Szeto +1
Lean 4's grind tactic combines congruence closure, E-matching, and case-splitting into a single automated solver, and like any such solver, it relies on hand-tuned heuristics to de…
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…