ProofCoder Verker - Overall: leaderboard
ProofCoder Verker - Overall: Lemmas proved (%). ProofCoder arXiv 2611.14106v1: proof pass percentages and obligation-specific pass rates, 200 SV-COMP and 80 Verker lemmas. Author reruns use Claude Sonnet 4.5 and GPT-6-sol, temperature 0. AutoRocq, ProofCoder tactic-level and whole-proof retain distinct runs; ProofCoder uses OpenCode plus custom Rocq MCP, Rocq 8.18. External Rango/PALM/etc rows and previously published GPT-4.1 are not recounted. Cost/time columns are not capability.
Metric: Lemmas proved (%). Source: arxiv.org. Saturation forecast: Rough model projection: around 2026. 6 models tracked.
Top models
| # | Model | Score | Overall rank |
|---|---|---|---|
| 1 | GPT-6-sol (Benchmark Sweep Run: source=proofcoder_paper; harness=Whole-Proof; temperature=0; reasoning=unreported; Rocq=8.18) | 60 | |
| 2 | GPT-6-sol (Benchmark Sweep Run: source=proofcoder_paper; harness=Tactic-Level; temperature=0; reasoning=unreported; Rocq=8.18) | 57.5 | |
| 3 | GPT-6-sol (Benchmark Sweep Run: source=proofcoder_paper; harness=AutoRocq; temperature=0; reasoning=unreported; Rocq=8.18) | 47.5 | |
| 4 | Claude Sonnet 4.5 (Benchmark Sweep Run: source=proofcoder_paper; harness=Tactic-Level; temperature=0; reasoning=unreported; Rocq=8.18) | 42.5 | |
| 5 | Claude Sonnet 4.5 (Benchmark Sweep Run: source=proofcoder_paper; harness=Whole-Proof; temperature=0; reasoning=unreported; Rocq=8.18) | 38.8 | |
| 6 | Claude Sonnet 4.5 (Benchmark Sweep Run: source=proofcoder_paper; harness=AutoRocq; temperature=0; reasoning=unreported; Rocq=8.18) | 36.2 |
Interactive version: theaggregate.ai/benchmark?slug=proofcoder-verker-overall · How It Works · Data refreshed daily, snapshot 2026-11-12.