Papers With

← All papers
First page of Ablation and the Meno: Tools for Empirical Metamathematics

Ablation and the Meno: Tools for Empirical Metamathematics

Zhengqin Fan, Simon DeDeo

cs.LO Apr 24, 2026 · v1
autoformalization theorem-proving-ml ai-agents analysis
Read PDF arXiv abstract Code
TL;DR
Meno, an MCP-orchestrated LLM autoformalizer, proves Lean 4 theorems and uses Lean metaprogramming to ablate tactics like Classical.choice.
Abstract
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.
Problem

Exploring the space of possible formal proofs for a theorem, and understanding how constraining available tactics changes proof strategies, lacks systematic tools. The relationship between human proofs and machine-generated alternatives is poorly characterized.

Approach

Meno is an LLM-based autoformalizer that takes a Lean theorem statement (optionally with an informal proof) and systematically searches for formal proofs via an MCP-orchestrated agent loop. Tactic ablation uses Lean metaprogramming to selectively disable tactics (e.g., Classical.choice), forcing alternative proof strategies. The resulting proof populations are embedded using Goedel Prover and analyzed via multidimensional scaling.

Figure 1: The space of proofs as found by Meno, both with and without ablation (open vs. solid circles), for the three proofs of Table 1 . Tao’s Lean proof is marked as a star.
Results

On three theorems from Tao's Analysis I, Meno produced 25-36 proofs per theorem under each condition. The proof populations lie on 1-2 dimensional submanifolds of the 5140-dimensional embedding space (2d MDS correlation r > 0.87), far from human-authored proofs. Ablating Classical.choice still yields comparable numbers of proofs (26-31) with distinct clustering patterns.

TheoremPlain (n)Ablated (n)2d MDS r
Russell's Paradox36290.912
X<2^X36310.876
Reals are complete25260.965
Proof counts and MDS fit quality