Ablation and the Meno: Tools for Empirical Metamathematics

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, a new method for exploring mathematical creativity under constraint. We show these tools in action on simple theorems found in Terrence Tao's Analysis I, selectively ablating solution paths associated with non-constructive proofs, and analyze the properties of the resulting population using Goedel Prover embeddings.