Cover Image

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Aniva, Leni, Oikawa, Iori, Dill, David, Barrett, Clark
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Machine Learning
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
by: Aniva, Leni, et al.
Published: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
by: Zhang, Liao, et al.
Published: (2024)

Proof Minimization in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
by: Zhang, Terry Jingchen, et al.
Published: (2025)

Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
by: Vishwakarma, Rahul, et al.
Published: (2023)

What are the Right Symmetries for Formal Theorem Proving?
by: Olejniczak, Krzysztof, et al.
Published: (2026)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
by: Lamont, Sean, et al.
Published: (2024)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
by: Dong, Kefan, et al.
Published: (2025)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
by: Zhao, Xueliang, et al.
Published: (2024)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
by: Rao, Balaji, et al.
Published: (2025)

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
by: Kasaura, Kazumi, et al.
Published: (2025)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

Process-Driven Autoformalization in Lean 4
by: Lu, Jianqiao, et al.
Published: (2024)

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
by: Rajaee, Sara, et al.
Published: (2025)

Lecture Notes on Verifying Graph Neural Networks
by: Schwarzentruber, François
Published: (2025)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Almost Surely Asymptotically Constant Graph Neural Networks
by: Adam-Day, Sam, et al.
Published: (2024)

Automated Tactics for Polynomial Reasoning in Lean 4
by: Shen, Hao, et al.
Published: (2026)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

The Descriptive Complexity of Graph Neural Networks
by: Grohe, Martin
Published: (2023)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
by: Pertseva, Elizaveta, et al.
Published: (2026)

Verifying Quantized Graph Neural Networks is PSPACE-complete
by: Sälzer, Marco, et al.
Published: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
by: Wu, Haoze, et al.
Published: (2024)

A Hybrid Real-Time Framework for Efficient Fussell-Vesely Importance Evaluation Using Virtual Fault Trees and Graph Neural Networks
by: Xiao, Xingyu, et al.
Published: (2024)

The Logical Expressiveness of Topological Neural Networks
by: Akbari, Amirreza, et al.
Published: (2026)

Space Explanations of Neural Network Classification
by: Labbaf, Faezeh, et al.
Published: (2025)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

Logic Gate Neural Networks are Good for Verification
by: Kresse, Fabian, et al.
Published: (2025)

Herald: A Natural Language Annotated Lean 4 Dataset
by: Gao, Guoxiong, et al.
Published: (2024)

The Polynomial Counting Capabilities of Message Passing Neural Networks
by: Sälzer, Marco, et al.
Published: (2026)

TLINet: Differentiable Neural Network Temporal Logic Inference
by: Li, Danyang, et al.
Published: (2024)

Branch and Bound for Piecewise Linear Neural Network Verification
by: Bunel, Rudy, et al.
Published: (2019)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)