Ablation and the Meno: Tools for Empirical Metamathematics
For researchers in automated theorem proving and mathematical creativity, this work provides tools to explore constrained proof spaces, but the results are preliminary and on simple theorems.
The paper introduces Meno, an autoformalizer that proves theorems in Lean by exploring formal and informal proofs, and tactic ablation, a method for studying mathematical creativity under constraint. Applied to theorems from Tao's Analysis I, they find that ablated proofs lie on low-dimensional submanifolds far from human constructions.
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. Among other things, our analysis of this novel population reveals that they lie on low (one or two) dimensional submanifolds of the much higher-dimensional representation space, and far away from their corresponding human constructions.