Introduces a finite set of atomic tactics, an atomization algorithm, and a GNN-based prover (Nazrin) trained on Lean standard library and Mathlib proofs.
Abstract
In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a statement in a proof assistant. In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving. We first present a set of atomic tactics, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a transposing atomization algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the ExprGraph data structure, which provides a succinct representation for Lean expressions. Finally, we present the Nazrin Prover, short for Neural Atomizer for Inhabitation Problems, a graph neural network-based theorem proving agent using atomic tactics and ExprGraph. Nazrin circumvents many challenges faced by existing proving agents by exclusively dispatching atomic tactics, and it is robust enough to both train and evaluate on consumer-grade hardware. We demonstrate the potential of tools like Nazrin using theorems from Lean's standard library and from Mathlib.
Problem
Machine-assisted theorem proving in Lean is hampered by the unbounded, noisy space of tactics used in human-written proofs, complicating training of proving agents. There is no compact, finite action space or expression representation suited to learning proof search.
Approach
The authors define a small finite set of atomic tactics sufficient to prove any provable Lean statement, and a transposing atomization algorithm that rewrites arbitrary proof terms into sequences of these atomic tactics. Lean expressions and goals are encoded via an ExprGraph data structure through an essentialization process that discards search-irrelevant information. A graph neural network agent, Nazrin Prover, consumes ExprGraphs and dispatches only atomic tactics; it uses Pantograph to interact with Lean 4.
Figure 6 : ExprGraph of \forall(p\,q:\mathsf{Prop}),p\lor q\to q\lor p . Notice that every subexpression corresponds to a locus (grey vertex) in this graph.
Results
Atomization succeeded on about 58% of 170,180 user-defined theorems from Lean's standard library and Mathlib. After training on one slice, Nazrin achieved 57% accuracy on a standard-library slice and 34% proof completion on a Mathlib slice, and proved theorems that Aesop and Grind could not.
