CAM-Bench (Pass@1): leaderboard

Metric: Pass@1 (%): probability that a single sampled whole proof makes the CAM-Bench Lean file compile under Lean 4 and Mathlib v4.28.0 with integrity checks, the unbiased estimate from 32 samples per target, over the 1,000 proof targets; higher is better. Source: arxiv.org. Saturation forecast: Around 2030. 5 models tracked.

Top models

#ModelScore
1Gemini 3.1 Pro (Preview)6.04
2DeepSeek V4 Pro5.78
3Claude Sonnet 4.65.14
4GPT-5.42.96
5Kimi K2.60.28

Interactive version: theaggregate.ai/benchmark?slug=cam-bench-pass-1 · How It Works · Data refreshed daily, snapshot 2026-10-07.