2 papers
cs.SE2026
VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
Yutong Xin, Qiaochu Chen, Greg Durrett +1
Large language models have achieved striking results in interactive theorem proving, particularly in Lean. However, most benchmarks for LLM-based proof automation are drawn from ma…
cs.PL2025
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin, Jimmy Xin, Gabriel Poesia +3
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-st…