VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
arXiv:2602.18307v2 Announce Type: replace-cross Abstract: Large language models have achieved striking results in interactive theorem proving, particularly in Lean. However, most benchmarks for LLM-ba