PutnamBench

The wiki's first formal-proving benchmark and, for reasonable budgets, still far from solved. Through most of 2024–2025 the best systems solved single digits of the Lean set (Goedel-Prover 7 at pass@512; GPT-4o ~1). General reasoning models at pass@1 remain low (GPT-5 ReAct ~28–42 of ~660, single digits %). Heavy-compute systems have since climbed steeply — ByteDance's Seed-Prover reportedly ~581/672 Lean at ~10 GPU-days per problem, and in Jan 2026 Logical Intelligence's Aleph CLAIMED 668/672 (99.4%, agentic pass@1) topping the board — but these use enormous or single-source, unreproduced budgets, and the Isabelle/Coq subsets and the harder 'no-answer' variant remain far less attacked. What would move this to nearing-saturation: independent reproduction of high solve rates across languages under disclosed, comparable budgets.