Showing cs.LGShow all
2 papers · 1 filter
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.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…