Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Shen, Austin, Shi, Yunong
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
by: Szeider, Stefan
Published: (2026)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
by: Yin, David, et al.
Published: (2025)

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

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

LeanTutor: Towards a Verified AI Mathematical Proof Tutor
by: Patel, Manooshree, et al.
Published: (2025)

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

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
by: Yanahama, Banri, et al.
Published: (2026)

ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
by: Cabral, Rafael, et al.
Published: (2025)

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
by: Lu, Jialin, et al.
Published: (2026)

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
by: Han, Sangjun, et al.
Published: (2025)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

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

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
by: Ospanov, Azim, et al.
Published: (2025)

Investigations into Proof Structures
by: Wernhard, Christoph, et al.
Published: (2023)

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

An Undecidability Proof for the Plan Existence Problem
by: Achilleos, Antonis
Published: (2026)

Large Language Model for OWL Proofs
by: Yang, Hui, et al.
Published: (2026)

Abstraction-Based Proof Production in Formal Verification of Neural Networks
by: Elboher, Yizhak Yisrael, et al.
Published: (2025)

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

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

Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism
by: Arkoudas, Konstantine, et al.
Published: (2026)

StepProof: Step-by-step verification of natural language mathematical proofs
by: Hu, Xiaolin, et al.
Published: (2025)

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

Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
by: Gonzalez, Salwa Tabet, et al.
Published: (2024)

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

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
by: Goertzel, Ben
Published: (2025)

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
by: Mayeux, Arnaud, et al.
Published: (2025)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

A Personalised Formal Verification Framework for Monitoring Activities of Daily Living of Older Adults Living Independently in Their Homes
by: Contreras, Ricardo, et al.
Published: (2025)

Combining Textual and Structural Information for Premise Selection in Lean
by: Petrovčič, Job, et al.
Published: (2025)

Where to Search: Measure the Prior-Structured Search Space of LLM Agents
by: Song, Zhuo-Yang
Published: (2025)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
by: Xin, Huajian, et al.
Published: (2024)

Efficient Neural Clause-Selection Reinforcement
by: Suda, Martin
Published: (2025)

Analyzing Value Functions of States in Parametric Markov Chains
by: Engelen, Kasper, et al.
Published: (2025)

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

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

The logic of KM belief update is contained in the logic of AGM belief revision
by: Bonanno, Giacomo
Published: (2026)

First Order Logic with Fuzzy Semantics for Describing and Recognizing Nerves in Medical Images
by: Bloch, Isabelle, et al.
Published: (2025)