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.

翻译：在机器辅助定理证明中，定理证明代理通过搜索表达式与策略的序列，以在证明辅助工具中完成猜想的证明。本研究针对机器辅助定理证明面临的若干障碍，提出了一系列创新性概念与能力。我们首先提出了一套**原子策略**——这是一个能够证明Lean中任何可证命题的有限小规模策略集合。随后，我们引入**转置原子化**算法，该算法可将任意证明表达式转化为原子策略序列。接着，我们提出**ExprGraph**数据结构，其为Lean表达式提供了简洁的表示形式。最后，我们提出**Nazrin证明器**——一个基于图神经网络、采用原子策略与ExprGraph的定理证明代理。Nazrin通过专一地调度原子策略，规避了现有证明代理面临的诸多挑战，且其鲁棒性足以在消费级硬件上完成训练与评估。我们通过Lean标准库及Mathlib中的定理案例，展示了Nazrin此类工具的潜在应用价值。