Ablation and the Meno: Tools for Empirical Metamathematics
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913059114582016 |
|---|---|
| author | Fan, Zhengqin DeDeo, Simon |
| author_facet | Fan, Zhengqin DeDeo, Simon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_22519 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Ablation and the Meno: Tools for Empirical Metamathematics Fan, Zhengqin DeDeo, Simon Logic in Computer Science History and Overview 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. |
| title | Ablation and the Meno: Tools for Empirical Metamathematics |
| topic | Logic in Computer Science History and Overview |
| url | https://arxiv.org/abs/2604.22519 |