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

Austin Shen, Yunong Shi

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) p…