Ablation and the Meno: Tools for Empirical Metamathematics

TL;DR

This paper introduces Meno, an autoformalizer for Lean, and tactic ablation to explore mathematical proof space and creativity, revealing insights into proof representations and their relation to human proofs.

Contribution

The paper presents Meno and tactic ablation as new tools for empirical metamathematics, enabling systematic exploration of proof spaces and analysis of mathematical creativity.

Findings

A population of ablated proofs lies on low-dimensional submanifolds in representation space.

Ablated proofs are significantly different from human proofs in their embedding space.

Meno effectively explores formal and informal proofs in Lean.

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.