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

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 arXiv:2605.25556v1 Announce Type: cross 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 co