Ablation and the Meno: Tools for Empirical Metamathematics

Zhengqin Fan, Simon DeDeo

We present the results from Meno, a simple autoformalizer that proves theorems in Lean by systematically exploring the space of both formal and informal proofs, and tactic ablation…