Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

arXiv:2602.18767v3 Announce Type: replace-cross 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 extbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a extbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the extbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the extbf{Nazrin Prover}, short for extbf{N}eural extbf{A}tomiextbf{z}eextbf{r} for extbf{In}habitation 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.

Source: arXiv cs.LG | 2026-07-01