Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

TL;DR

Nazrin introduces a novel approach to machine-assisted theorem proving in Lean by using atomic tactics, a new proof expression representation, and a graph neural network-based prover, enabling efficient and robust proof search.

Contribution

The paper presents atomic tactics, a transposing algorithm, the ExprGraph data structure, and the Nazrin prover, advancing the capabilities of neural theorem proving in Lean.

Findings

Nazrin can prove theorems from Lean's standard library.

The approach is robust on consumer-grade hardware.

Atomic tactics simplify proof search and representation.

Abstract

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.