Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

2026/02/21 by Leni Aniva, Iori Oikawa, David Dill +1 · 2 voices
Computer Science · #cs.LO #cs.LG

paper · pdf

arxiv published 2026/02/21 · arxiv updated 2026/06/30

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 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.

Citations

• GraphMind: Theorem Selection and Conclusion Generation Framework with Dynamic GNN for LLM Reasoning
• A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
• Lean-SMT: An SMT tactic for discharging proof goals in Lean
• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
• BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
• Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
• HyperTree Proof Search for Neural Theorem Proving
• The lean mathematical library
• Graph Representations for Higher-Order Logic and Theorem Proving

Discussions

• Transposing Atomization is here! We show that GNNs equipped with atomic tactics can do theorem proving in #leanlang. #MATP arxiv.org/abs/2602.18767 [bsky, 4 points, 0 comments]
• どうも東方オタクの数学者が定理証明支援系周りで活躍しているらしい。 [2602.18767] Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 https://arxiv.org/abs/2602.18767 [bsky, 3 points, 0 comments]

Related

• Proof Artifact Co-training for Theorem Proving with Language Models
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
• Leanabell-Prover: Posttraining Scaling in Formal Reasoning