# Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

arXiv: https://arxiv.org/abs/2602.18767 · HTML: https://mlsanity.com/paper/2602.18767/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 25 references that are in the map.
- First posted on arXiv 21 Feb 2026.

## Builds on (most cited first, 11 of 11)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [Lean-SMT: An SMT tactic for discharging proof goals in Lean](https://mlsanity.com/paper/2505.15796/) (2025)
- [Lean-auto: An Interface between Lean 4 and Automated Theorem Provers](https://mlsanity.com/paper/2505.14929/) (2025)
- [A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL](https://mlsanity.com/paper/2507.18885/) (2025)
- [GraphMind: Theorem Selection and Conclusion Generation Framework with Dynamic GNN for LLM Reasoning](https://mlsanity.com/paper/2511.19078/) (2025)

## Abstract (arXiv)

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.