What the public evaluation establishes

One harness, two benchmark settings

The reported default model is claude-opus-4-7, with Lean 4 v4.28.0 and Mathlib v4.28.0. The harness uses no model fine-tuning, custom reinforcement-learning objective, or theorem-specific scaffolding. Its input is an already formalized Lean statement with an unfinished proof.

FormalQualBench contains 23 qualifying-exam theorems; the Putnam experiment uses the 12 problems from 2025. The default budget is four hours per problem. The tables identify the FormalQualBench extension beyond that budget, and all reported solves undergo the same final audit.

FormalQualBench: separate the matched budget from the extension

Nine problems close within four hours. A tenth, ID 9, closes after 4h40m. Reporting both numbers keeps the extra solve visible without treating it as a four-hour success. The remaining 13 problems are not reported as solved.

Putnam 2025: twelve completed proofs, unequal effort

All twelve problems close. Their recorded times sum to 789 minutes, or 13h09m; this is a sum of per-problem wall-clock times, not the elapsed duration of a parallel batch. A5 and B1 account for 396 minutes, slightly over half of that sum.

How stable is a successful run?

The paper repeats four selected FormalQualBench problems eight times each. All 32 attempts produce clean proofs, but their running times vary. This measures repeatability on that selected subset, not across all 23 problems or within a uniform four-hour limit.

Cost, library support, and the next questions

Across the ten successful FormalQualBench runs, the paper reports USD 1,183.45 of API spend and 19h54m of summed time. Those totals cover the solved subset, not all attempted benchmark problems. Repeated compilation, replanning, and context traffic make longer proof plans expensive.

A cheaper model does not necessarily produce a cheaper proof. On FormalQualBench ID 7, Haiku takes 4h34m and USD 26.24, compared with Opus at 16m and USD 13.53; the reported plans contain nine and three statements respectively. On harder examples, the available model and usable Mathlib lemmas remain limiting factors.

Natural next steps are to reduce redundant work, test Lean-specialized or lower-cost models, and use failed decompositions to locate missing or hard-to-find library facts. A further question is how to present a completed formal proof so that its mathematical ideas are easier for a person to understand.