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

• URL: http://arxiv.org/abs/2605.25556v2
• Date: Wed, 27 May 2026 19:06:07 GMT
• Title: Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
• Abstract summary: We introduce proof-state snapshotting, which captures the elaborated proof state once and reuses it across branches via a small extension to the Lean 4 language server.<n>Across 48 miniF2F-v2 problems, our approach achieves a 5.6-50x wall-time speedup over the standard fallback.
• Score: 1.2816802110958607
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) pipelines. In current systems, each search branch reconstructs a proof state by re-running elaboration, leading to substantial per-branch overhead. In Lean 4 with Mathlib, this cost has two components: (1) import loading, which deserializes pre-compiled libraries (~60 s per branch); and (2) theorem-body elaboration, which re-checks the theorem context up to the target goal (estimated 18-735 s depending on proof complexity). Together, these account for >99% of per-branch wall time, making portfolio-based search impractical at scale. We observe that this overhead arises from a mismatch between the structure of proof search and its execution model: branching is implemented via repeated reconstruction of proof states rather than direct reuse. To address this, we introduce proof-state snapshotting, which captures the elaborated proof state once and reuses it across branches via a small extension to the Lean 4 language server. Across 48 miniF2F-v2 problems (45 prove-phase benchmarks and 3 full end-to-end runs), our approach achieves a 5.6-50x wall-time speedup over the standard fallback (average 14x, median 9.7x). Speedup increases with the number of proof branches. Our method is orthogonal to import-level caching (e.g., Kimina Lean Server), which avoids import loading but not theorem-body elaboration. The patched Lean binary and the Snapshot-DSP pipeline will be released as open source upon publication.

Related papers

• PARSER: Read in Parallel, Reason in Depth for Long-Context LLM Agents [85.82624962221026]
  We introduce PARSER, which decouples reading from reasoning.<n>A bank of lightweight subagents each bound to a single chunk read the entire document in parallel.<n>On multi-hop QA with contexts ranging from 7K to 896K tokens, PARSER with a 4B backbone outperforms the strongest sequential memory baseline.
  arXiv  Detail & Related papers  (2026-09-06T16:19:01Z)
• Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing [5.8296917468117835]
  We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle.<n>Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation.<n>Our method achieves 87.1% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget.
  arXiv  Detail & Related papers  (2026-08-11T04:28:22Z)
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
  ITPEval is the first benchmark for evaluating automated formal proof translation across four major ITPs.<n>We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends.
  arXiv  Detail & Related papers  (2026-07-07T22:05:55Z)
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
  We introduce Goedel-Architect, a framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement.<n>Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench.<n>This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.
  arXiv  Detail & Related papers  (2026-06-04T17:54:44Z)
• OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
  OProver is a unified framework for agentic formal iteration theorem proving in Lean 4.<n>It runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL.<n>OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.
  arXiv  Detail & Related papers  (2026-05-17T06:39:05Z)
• LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving [7.326381497366569]
  Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof.<n>We present LeanSearch v2, a two-mode retrieval system for this task.
  arXiv  Detail & Related papers  (2026-05-13T08:04:57Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.<n>We propose a hierarchical proof search framework for automated code verification in Lean4.<n>We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion.
  arXiv  Detail & Related papers  (2026-03-18T18:42:04Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• dParallel: Learnable Parallel Decoding for dLLMs [77.24184219948337]
  Diffusion large language models (dLLMs) offer parallel token prediction and lower inference latency.<n>Existing open-source models still require nearly token-length decoding steps to ensure performance.<n>We introduce dParallel, a simple and effective method that unlocks the inherent parallelism of dLLMs for fast sampling.
  arXiv  Detail & Related papers  (2025-09-30T16:32:52Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  We introduce LeanProgress, a method that predicts the progress in the proof.<n>Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1%.
  arXiv  Detail & Related papers  (2025-02-25T07:46:36Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.