Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

Clark Barrett; David Dill; Iori Oikawa; Leni Aniva

REVIEW 4 major objections 5 minor 12 references

Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

T0 review · 4 major / 5 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A finite menu of atomic tactics can, in principle, replay any provable Lean proof, and a GNN agent trained on atomized traces proves theorems on a laptop.

desk verdict A genuinely novel finite-action-space pipeline for Lean proving, but the abstract's completeness claim is contradicted by the paper's own 58% atomization rate, so the central assertion needs to be scaled back and the artifacts released before this is fully believable. read the letter →

arxiv 2602.18767 v3 pith:UAJKOR6G submitted 2026-02-21 cs.LO cs.LG

Leni Aniva , Iori Oikawa , David Dill , Clark Barrett This is my paper

classification cs.LOcs.LG MSC 03B3568T0168T07

keywords Lean4atomictacticsatomizationExprGraphneuralnetworkstheoremprovingproofsearchmetavariablecoupling

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that interactive theorem proving in Lean 4 can be recast as a finite, low-entropy decision problem: every provable statement admits a proof built from a small fixed set of atomic tactics, each corresponding to one top-level constructor of a proof term. To turn that theoretical claim into practice, the paper presents a transposing atomization algorithm that rewrites ordinary proof terms into sequences of atomic tactic applications, and a graph representation that keeps only the information needed to choose the next tactic. The payoff is Nazrin, a graph-neural-network agent that learns to dispatch atomic tactics from atomized training data and can train and search on consumer-grade hardware while proving theorems that existing automation in the proof assistant cannot discharge. A sympathetic reader would care because the atomic-tactic move dissolves two standard obstacles in machine learning for proofs: an unbounded tactic space and noisy, human-stylized proof traces.

What carries the argument

The load-bearing mechanism is a direct mapping from proof-term constructors to tactics: each top-level constructor (lambda, pi, application, projection, let, and so on) is paired with one atomic tactic that introduces it, making the action space finite. Two hand-built tactics, tailArg and motivatedApply, avoid Lean's aggressive unification by constructing raw applications and equality conduits; the grades defined by the paper (holo/semi, prograde/retrograde) tell the atomizer which tactic orderings are freely swappable, enabling goal-level transposition around unification dead ends. ExprGraph supplies structural guarantees — symmetry, self-similarity, locus conservation, condensation — so th

What would settle it

Take a provable Lean theorem whose proof term, under the atomizer's semigrade/holograde strategy, reaches a state where no atomic tactic can be found and the goal cannot be deferred, or where the 3000-step cap is exceeded; such a theorem is already a counterexample to the claimed completeness of atomization.

Watch

Extended reading notes

Core claim

The paper's central claim is completeness of the atomic tactic set: because every Lean proof term is ultimately built from a small set of expression constructors, and each constructor can be introduced by exactly one atomic tactic, any provable theorem can in principle be proved by a finite sequence of actions drawn from a fixed menu. The transposing atomization algorithm is the bridge from that claim to data: it takes a ground-truth proof term, processes goals in a successor-first order, and when unification would block a step it uses synthetic tactics and goal-level transposition to keep going. The paper pairs this with ExprGraph, a graph encoding of expressions that identifies alpha-equiv

Load-bearing premise

The whole pipeline stands on the claim that the atomization heuristics can decompose any proof term into atomic tactics; the paper's own evaluation reports success on only about 58% of the corpus under a 3000-step cap, so anything that needs the remaining 42% is not yet supported.

Editorial extensions

If this is right

If atomic tactics are complete, any theorem-proving agent can be framed as a finite-action decision problem, removing the need to generate arbitrary tactic syntax.
Atomization converts existing human-written proofs into search-view training traces, so a model learns how proofs are found rather than how they are presented.
Expressions and goals can be essentialized into graphs that are invariant under alpha-equivalence and search-view equivalence, reducing training noise and sample complexity.
Atomized trace length and maximum cross-section give a principled proof-difficulty metric that heavy compound tactics cannot hide.
A high-throughput GNN prover trained this way can run on CPU-only hardware and solve goals that existing automation inside the proof assistant cannot discharge.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If atomization coverage can be lifted beyond the reported ~58%, the same data pipeline would scale automatically with any formal library: every newly formalized theorem becomes additional supervised training data without manual annotation.
The goal-level transposition ordering suggests a testable curriculum: atomized traces with minimized cross-section should be easier for a small model to learn, so an ablation that randomizes goal order within atomization should hurt accuracy if transposition is doing real work.
ExprGraph's condensation and locus-conservation principles may transfer to other dependently typed proof assistants; a direct test would be reusing the encoding on a second system and checking whether the same atomic-tactic schedule applies.
The rainbow guidance heuristic could be replaced by a learned goal-ranking head, and the paper's own architecture notes suggest this as a natural extension.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take on the Nazrin paper. The atomic-tactics idea is real: a finite action space keyed to Lean's expression constructors, plus the transposing atomization algorithm that rewrites arbitrary proofs into those tactics, and the ExprGraph representation. Those are genuine engineering contributions, not re-coordinatized prior work. The GNN prover trained on atomized traces is a sensible low-resource design, and the held-out slice generalization evaluation is an honest attempt; they also compare against Aesop and Grind as external baselines.

The soft spot is the completeness claim, and it is not minor. The abstract says the tactic set is 'capable of proving any provable statement in Lean' and that atomization 'turns arbitrary proof expressions into a series of atomic tactics.' The paper never proves the first claim; Table 1 is a correspondence table, not a proof. More importantly, the paper's own numbers contradict the second: Section 6 reports a 58% atomization success rate under a 3000-step cap, and Section 7 says 'Atomization does not yet work for all theorems.' Section 4.2 defers goals with no atomic tactic and only 'hopefully' revisits them. So the load-bearing assertion in the abstract is false as stated. This is a presentation flaw rather than a fatal one — the approach can be reframed as 'broad-coverage atomic tactics' — but the overclaim is severe enough that referees should insist on a rewrite.

Other soft spots: no code or data released, so the 58% and the 34% proof-completion rate cannot be checked; no error bars on the evaluations; and the authors concede Grind was at a disadvantage in the comparison. The cross-section difficulty metric is plausible but not validated as a predictor. None of these are fatal by themselves, but together they mean the empirical case is suggestive, not conclusive.

Who should read it: anyone building neural or symbolic automation for Lean, especially the non-LLM / graph-based line of work. The atomization pipeline could be reused even if the prover itself doesn't scale.

Recommendation: send it to serious peer review. The novel parts deserve scrutiny, and the overclaim needs correcting before publication. I'd want the artifacts released before accepting; without them, the empirical results are hard to evaluate.

Referee Report

4 major / 5 minor

Summary. The paper introduces a complete-in-principle finite set of 'atomic tactics' for Lean 4, a 'transposing atomization' algorithm that converts proof terms into sequences of these tactics, a graph-based expression representation called ExprGraph, and the Nazrin Prover, a GNN-based agent that searches over the atomic tactic space. The authors claim the atomic tactic set is capable of proving any provable statement in Lean and that atomization turns arbitrary proof expressions into atomic tactic traces. They evaluate Nazrin on standard library and Mathlib slices, reporting 57% and 34% completion rates respectively and showing complementary performance against Aesop and Grind. The paper is clearly written and the overall direction is appealing, but the central completeness and atomization claims are asserted rather than proven and appear to be contradicted by the paper's own evaluation numbers.

Significance. If the completeness of the atomic tactic set and the correctness of the atomization algorithm were established, this would be a significant contribution to neural theorem proving: a genuinely finite action space would simplify training, enable high-throughput search on consumer hardware, and make agent behavior more diagnosable. The paper also contributes the ExprGraph representation and the NPA architecture, which are interesting and potentially reusable design ideas. The evaluation uses held-out slices and external baselines, which is a methodological strength relative to pure benchmark reporting. However, the paper does not ship machine-checked proofs of the completeness claims, and the 58% atomization success rate directly undermines the 'any provable statement' claim. The contribution is therefore promising but currently overclaimed; the central claims need either rigorous proof or careful qualification.

major comments (4)

[Abstract and §4.1 (Table 1)] The abstract claims atomic tactics are 'capable of proving any provable statement in Lean' and that atomization 'turns arbitrary proof expressions into a series of atomic tactics.' Section 4.1 bases completeness on Table 1, but the table's 'Invalid' and 'Unfold' rows are not atomic tactics; the text only says they can be transformed, with no proof of preservation of provability or termination. Section 6 reports a 58% atomization success rate under a 3000-step cap, and §7 states 'Atomization does not yet work for all theorems.' Thus the central load-bearing claim is unproven and internally contradicted by the paper's own evaluation. This must be fixed either by a rigorous completeness argument or by explicitly qualifying the claim to the atomizable subset.
[§4.2, Listing 1] The defer mechanism in the atomization pseudocode is not a valid search procedure. When `atomize_step` returns `:defer`, the goal is yielded but never pushed back into `pending`; the loop terminates when `pending` is empty. The text says the goal is deferred 'hopefully becoming solvable later,' but no mechanism to revisit deferred goals is present. Either the pseudocode omits a reinsertion step, or atomization simply fails on any goal that cannot be immediately decomposed. This is a load-bearing detail because the algorithm's termination and success are what justify the training-data pipeline. A corrected pseudocode and a termination argument are needed.
[§6, evaluation universe] The paper reports a 57% completion rate on stdlib slice 2 and 34% on Mathlib slice 4, but it never states whether the evaluation sets are restricted to theorems that atomization succeeded on. If the model is evaluated on all theorems but trained only on the 58% that atomize, then the reported rates conflate the model's search ability with the coverage of the atomization pipeline. Conversely, if evaluation is restricted to atomizable theorems, the claim that Nazrin proves theorems that other automation tactics cannot is less informative. The paper should clearly separate the two settings and report accuracy on both the atomizable subset and the full slice.
[§6, Figure 10 and Grind comparison] The comparison with Aesop and Grind is not fully controlled: the footnote states that 'for Aesop and Nazrin, we use perfect premise selection,' while Grind has no easy equivalent, so Grind is at a disadvantage in the experiment. This limits the strength of the claim that Nazrin is complementary or superior. The authors should either provide a comparison without perfect premise selection for all systems or explicitly state that the comparison is only a proof-of-concept, not a head-to-head evaluation.

minor comments (5)

[Throughout] Numerous typos: 'imlplements' (Introduction), 'mathemtaical' (Introduction), 'assignd' (§3.1), 's mysterious' (§3.3), 'dicsuss' (Figure 1 caption), 'mesaured' (§6), and the broken spacing 'pr oo fex pr' in Listing 1. A careful proofread is needed.
[Title/header and DOI] The paper uses the placeholder '42nd Conference on Very Important Topics (CVIT 2016)' and DOI '10.4230/LIPIcs.CVIT.2016.23'. These must be replaced with real venue and DOI information before publication.
[References] Reference [11] is malformed: it lists only editors and no title/authors for the Lean 4 manual. Reference [1] is incomplete. Several references lack page numbers or full bibliographic details.
[§4.2, code availability] The paper says 'Code will be released after the anonymous review period.' This is acceptable, but the pseudocode in Listing 1 omits the definitions of `try_semigrade` and `try_holograde`, which are the core of the algorithm. Please include more detailed pseudocode or an appendix describing these functions so the algorithm is reproducible from the paper itself.
[§5.2, Figure 8] The NPA diagram is hard to interpret. In particular, the 'Exit reduceBeta, abandon' state and the transitions between states are not clearly explained in the text. Please add a description of the states and their semantics.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the claimed reduction chain is self-contained; the abstract's sweeping atomization claim is unsupported by the paper's own limitation, but that is not equation-level circularity.

full rationale

No circular step found. The derivation chain is: (1) a finite atomic tactic set is defined so that each Lean expression constructor has a corresponding tactic (Table 1); (2) the transposing atomization algorithm consumes a ground-truth proof term and emits an atomic tactic trace (Listing 1); (3) the GNN/Nazrin agent is trained on those atomized traces; (4) generalization is measured on held-out next-slice theorems, with external comparisons against Aesop and Grind. None of these steps fits a parameter to the quantity it later claims to predict. Atomic-tactic completeness is argued by construction from expression constructors, not by fitting. The training labels come from the authors' own atomization framework, which can bias coverage, but this is not a reduction of a predicted quantity to a fitted constant. The only self-citation, Pantograph [2], is used for terminology and as an interface to Lean; it is not load-bearing for the completeness claim. The paper's own evaluation weakens the abstract's unqualified wording: Section 6 reports 'The success rate of atomization is about 58%' and Section 7 says 'Atomization does not yet work for all theorems.' This is an internal inconsistency between the abstract and the limitations, and it is a real correctness/support concern, but it is not circularity: a heuristic's failure does not make the atomic-tactic set self-definitional with respect to its training targets. Because no specific derivation reduces to its own inputs, the circularity score is 0.

Assumptions & free parameters 3 free parameters · 4 assumptions · 3 invented entities

The central contribution rests on the atomic-tactic completeness assumption and on the atomization pipeline's success; the GNN's trained weights and hand-chosen hyperparameters determine the empirical numbers. No hidden physical entities are introduced; the ledger entries are design constructs whose adequacy is asserted rather than independently verified.

free parameters (3)

GNN architecture hyperparameters = embedding_dim=32, layers=5, heads=4, gelu
Chosen by hand in Section 5.2; no sensitivity analysis reported; performance numbers depend on them.
training epochs = 100
Section 6: trained on stdlib slice 1 for 100 epochs; no early stopping or sweep reported.
atomization step limit = 3000
Section 6: cap on atomization steps; contributes to the 58% success rate.

assumptions (4)

domain assumption Lean 4's kernel correctly implements the Calculus of Inductive Constructions, so a term checked by Lean is a valid proof.
The whole pipeline trusts the soundness of Lean's kernel.
ad hoc to paper Every top-level constructor of a Lean proof term is covered by the atomic tactics in Table 1, and the Invalid/Unfold constructors can always be handled by the listed tactics.
Completeness claim in Section 4.1 and Table 1; stated without a formal proof.
ad hoc to paper The transposing atomization algorithm's ordering and deferral heuristics preserve provability and eventually terminate with a valid atomic proof whenever the algorithm reports success.
Listing 1 and Section 4.2; the algorithm can return 'defer' and can fail, so this assumption applies only to reported successes.
domain assumption ExprGraph essentialization erases exactly the information that is irrelevant to proof search, so the GNN is not missing decision-relevant content.
Section 5.1; no formal equivalence proof between kernel/search view and ExprGraph.

invented entities (3)

Atomic tactics (the finite tactic set in Figures 2 and 3)
purpose: Restrict agent actions to a finite, claimed-complete set
New construct; completeness asserted but not machine-checked; no external validation.
ExprGraph
purpose: Graph representation of Lean expressions for the GNN
New data structure; its sufficiency for tactic prediction is not independently validated.
Neural Probabilistic Automaton (NPA)
purpose: Use GNN heads to generate parameterized atomic tactics
New architecture concept; no separate benchmark.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4." pith.science (2026). https://pith.science/paper/UAJKOR6G

@misc{pith2026260218767,
  author       = {Pith},
  title        = {Pith review of: Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UAJKOR6G}},
  note         = {Machine review of arXiv:2602.18767}
}

read the original 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 \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}, short for \textbf{N}eural \textbf{A}tomi\textbf{z}e\textbf{r} for \textbf{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.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

12 extracted references · 2 canonical work pages

[3]

6 Jannis Limperg and Asta Halkjær From

URL:https://arxiv.org/abs/2511.19078,arXiv:2511.19078. 6 Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, page 253–266, New York, NY, USA,

arXiv 2023
[6]

9 REBECCA LEA MORRIS

URL:https://arxiv.org/abs/2505.15796,arXiv:2505.15796. 9 REBECCA LEA MORRIS. Motivated proofs: what they are, why they matter and how to write them.The Review of Symbolic Logic, 13(1):23–46, November

arXiv
[7]

10 Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy

URL: http: //dx.doi.org/10.1017/S1755020319000583,doi:10.1017/s1755020319000583. 10 Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving.Proceedings of the AAAI Conference on Artificial Intelligence, 34(03):2967–2974, Apr

work page doi:10.1017/s1755020319000583
[9]

14929,arXiv:2505.14929

URL:https://arxiv.org/abs/2505. 14929,arXiv:2505.14929. 13 Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. InProceedings of the 61st Annual Meeting o...

arXiv
[10]

URL: https://aclanthology.org/2023.acl-long.706,doi:10.18653/v1/2023.acl-long.706

Association for Computational Linguistics. URL: https://aclanthology.org/2023.acl-long.706,doi:10.18653/v1/2023.acl-long.706. 14 Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large- scale synthetic data,

doi:10.18653/v1/2023.acl-long.706 2023
[12]

16 Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar

URL:https://arxiv.org/abs/2502.03438,arXiv:2502.03438. 16 Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with CVIT 2016 23:18 Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 retrieval-augmented language models.Advan...

arXiv 2016
[2016]

08415,arXiv:1606.08415

URL:http://arxiv.org/abs/1606. 08415,arXiv:1606.08415. 4 Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving, 2022.arXiv:2205.11491. 5 Yutong Li, Yitian Zhou, Xudong Wang, GuoChen, and Caiyan Qin. Graphmind: Theorem s...

arXiv 2022
[2019]

org/abs/1910.09336,arXiv:1910.09336

URL:http://arxiv. org/abs/1910.09336,arXiv:1910.09336. 8 Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. Lean-smt: An smt tactic for discharging proof goals in lean,

arXiv 1910

Show all 12 references

[2020]

php/AAAI/article/view/5689,doi:10.1609/aaai.v34i03.5689

URL:https://ojs.aaai.org/index. php/AAAI/article/view/5689,doi:10.1609/aaai.v34i03.5689. 11 André Platzer and Geoff Sutcliffe, editors.The Lean 4 Theorem Prover and Programming Language, Cham,

doi
[2023]

7 mathlib

Association for Computing Machinery.doi:10.1145/3573105.3575671. 7 mathlib. The lean mathematical library.CoRR, abs/1910.09336,

1910
[2024]

15 Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen

URL:https://arxiv.org/abs/2405.14333,arXiv:2405.14333. 15 Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving,

arXiv
[2025]

3 Dan Hendrycks and Kevin Gimpel

URL: https://arxiv.org/abs/2410.16429, arXiv: 2410.16429. 3 Dan Hendrycks and Kevin Gimpel. Bridging nonlinearities and stochastic regularizers with gaussian error linear units.CoRR, abs/1606.08415,

arXiv

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.

[1] [3]

6 Jannis Limperg and Asta Halkjær From

URL:https://arxiv.org/abs/2511.19078,arXiv:2511.19078. 6 Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, page 253–266, New York, NY, USA,

arXiv 2023

[2] [6]

9 REBECCA LEA MORRIS

URL:https://arxiv.org/abs/2505.15796,arXiv:2505.15796. 9 REBECCA LEA MORRIS. Motivated proofs: what they are, why they matter and how to write them.The Review of Symbolic Logic, 13(1):23–46, November

arXiv

[3] [7]

10 Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy

URL: http: //dx.doi.org/10.1017/S1755020319000583,doi:10.1017/s1755020319000583. 10 Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving.Proceedings of the AAAI Conference on Artificial Intelligence, 34(03):2967–2974, Apr

work page doi:10.1017/s1755020319000583

[4] [9]

14929,arXiv:2505.14929

URL:https://arxiv.org/abs/2505. 14929,arXiv:2505.14929. 13 Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. InProceedings of the 61st Annual Meeting o...

arXiv

[5] [10]

URL: https://aclanthology.org/2023.acl-long.706,doi:10.18653/v1/2023.acl-long.706

Association for Computational Linguistics. URL: https://aclanthology.org/2023.acl-long.706,doi:10.18653/v1/2023.acl-long.706. 14 Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large- scale synthetic data,

doi:10.18653/v1/2023.acl-long.706 2023

[6] [12]

16 Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar

URL:https://arxiv.org/abs/2502.03438,arXiv:2502.03438. 16 Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with CVIT 2016 23:18 Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4 retrieval-augmented language models.Advan...

arXiv 2016

[7] [2016]

08415,arXiv:1606.08415

URL:http://arxiv.org/abs/1606. 08415,arXiv:1606.08415. 4 Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving, 2022.arXiv:2205.11491. 5 Yutong Li, Yitian Zhou, Xudong Wang, GuoChen, and Caiyan Qin. Graphmind: Theorem s...

arXiv 2022

[8] [2019]

org/abs/1910.09336,arXiv:1910.09336

URL:http://arxiv. org/abs/1910.09336,arXiv:1910.09336. 8 Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. Lean-smt: An smt tactic for discharging proof goals in lean,

arXiv 1910