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…