Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
This work addresses obstacles in theorem proving for users of proof assistants like Lean, though it appears incremental as it builds on existing graph neural network methods with new data structures and tactics.
The paper tackled the problem of machine-assisted theorem proving by introducing atomic tactics and a graph neural network-based agent called Nazrin, which can prove any provable statement in Lean and is designed to run on consumer-grade hardware, demonstrating its potential on theorems from Lean's standard library and Mathlib.
In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture 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 \textbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a \textbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the \textbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the \textbf{Nazrin Prover}, 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.