![[2602.18767] Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2602.18767] Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
Summary
The paper presents Nazrin, a graph neural network-based theorem proving agent that utilizes atomic tactics to enhance machine-assisted theorem proving in Lean 4.
Why It Matters
This research addresses significant challenges in theorem proving by introducing atomic tactics and a novel data structure, ExprGraph, which could improve the efficiency and accessibility of theorem proving tools, making them more robust for users with standard hardware.
Key Takeaways
- Nazrin introduces atomic tactics that can prove any provable statement in Lean.
- The transposing atomization algorithm converts complex proofs into atomic tactics.
- ExprGraph provides a concise representation of Lean expressions, enhancing processing efficiency.
- Nazrin is designed to operate effectively on consumer-grade hardware, broadening accessibility.
- The paper demonstrates Nazrin's capabilities using examples from Lean's standard library.
Computer Science > Logic in Computer Science arXiv:2602.18767 (cs) [Submitted on 21 Feb 2026] Title:Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 Authors:Leni Aniva, Iori Oikawa, David Dill, Clark Barrett View a PDF of the paper titled Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4, by Leni Aniva and 3 other authors View PDF HTML (experimental) 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 ...
