Showing 2026Show all
3 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.IR2026
TheoremGraph: Bridging Formal and Informal Mathematics
Simon Kurgan, Evan Wang, Eric Leonen +6
Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while forma…
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…