Date: March 2026
Dataset: 317 problems from Polya & Szego, Problems and Theorems in Analysis I (1925)
Task: Formalize each problem as a Lean 4 theorem statement (with sorry proof)
Arbiter: Claude Opus 4.6 (semantic correctness evaluation)
Seven frontier LLMs independently formalize each problem in Lean 4, given the problem text and book solution. A separate arbiter (Claude Opus 4.6) evaluates whether each formalization faithfully captures the mathematical content — correct types, hypotheses, quantifier structure, and conclusion.
Of the 317 problems in the experiment, 64 have corrupted input (garbled OCR, mismatched problem/solution pairs, truncated text) and 31 lack arbiter evaluations. We report results on the 222 clean problems where the input is well-formed and all evaluations are complete.
| Model | Correct | Partial | Wrong | Missing | Success Rate |
|---|---|---|---|---|---|
| GPT-5.4 | 85 | 1 | 14 | 122 | 38.3% |
| Gemini 3.1 Pro | 84 | 17 | 19 | 102 | 37.8% |
| Claude Opus 4.6 | 58 | 15 | 50 | 99 | 26.1% |
| Kimi k2 | 39 | 13 | 70 | 100 | 17.6% |
| GLM-5 | 22 | 17 | 84 | 99 | 9.9% |
| MiniMax | 22 | 14 | 87 | 99 | 9.9% |
| DeepSeek R1 | 21 | 12 | 90 | 99 | 9.5% |
"Missing" = no model output (API failure/timeout). "Partial" = captures some but not all mathematical content.
- GPT-5.4 and Gemini 3.1 Pro are nearly tied at ~38%, with 4x the success rate of the bottom tier.
- Reasoning-heavy models underperform. DeepSeek R1 and MiniMax — both known for extended chain-of-thought — score worst. Spending tokens on informal mathematical reasoning appears to hurt formalization precision.
- Claude Opus 4.6 sits in a clear middle tier at 26%.
- Gemini produces the most "partial" verdicts (17), suggesting it attempts more ambitious formalizations that capture some of the problem content even when incomplete.
| Category | Count |
|---|---|
| All 7 models correct | 3 |
| All 7 models wrong | 8 |
| Mixed (1–6 correct) | 112 |
The 8 unanimously wrong problems on clean input are genuinely difficult formalization challenges (Cauchy-Riemann equations in Lean, Weyl equidistribution, Bessel function asymptotics, coefficient domination for power series).
| Failure Mode | Count | Description |
|---|---|---|
| wrong_conclusion | 238 | Correct setup, wrong final statement |
| other | 168 | Miscellaneous (hallucinated problem, structural issues) |
| missing_hypothesis | 118 | Drops necessary conditions |
| wrong_type | 96 | Type errors: ℝ vs ℂ, ℕ vs ℤ, Finset vs Set |
| extra_hypothesis | 74 | Adds spurious constraints |
| constructive_vs_existence | 16 | Uses ∃ for "find"/"compute" problems |
| wrong_hypothesis | 15 | Replaces a condition with something different |
| quantifier_structure | 8 | ∀/∃ nesting or direction wrong |
$\displaystyle\sum_{k=0}^{n}(-1)^{n-k} 2^{2k}\binom{n+k+1}{2k+1}=n+1$
All 7 models produce essentially the same correct formalization:
theorem polya_szego_problem_39 (n : ℕ) :
∑ k in Finset.range (n + 1),
((-1 : ℤ) ^ (n - k)) * (2 : ℤ) ^ (2 * k) *
(Nat.choose (n + k + 1) (2 * k + 1) : ℤ) = ((n + 1 : ℕ) : ℤ) := by
sorryWhy it's easy: The problem is its formalization. No implicit hypotheses, no domain ambiguity, no constructive/existential distinction. The only creative decision is choosing ℤ for the alternating sign.
A subsequence whose terms are the successive partial sums of an absolutely convergent series can be picked out from every convergent sequence.
A clear statement from Part One. Only GPT-5.4 gets it right (1/7).
theorem convergent_sequence_has_subsequence_of_partial_sums
{u : ℕ → ℝ} {l : ℝ} (hu : Tendsto u atTop (𝓝 l)) :
∃ φ : ℕ → ℕ, ∃ a : ℕ → ℝ,
StrictMono φ ∧ HasSum a l ∧ Summable (fun n => |a n|) ∧
∀ n : ℕ, u (φ n) = ∑ i in Finset.range (n + 1), a i := by
sorryCorrectly captures: strictly monotone subsequence selector φ, absolutely convergent series a, and partial sums matching the subsequence.
theorem polya_szego_104 {a : ℕ → ℝ}
(ha : ∃ L, Filter.Tendsto a Filter.atTop (nhds L)) :
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (b : ℕ → ℝ),
Summable (fun n => |b n|) ∧
∀ n, a (φ n) = ∑ i ∈ Finset.range n, b i := by
sorryThe bug: Finset.range n sums {0, ..., n-1}, so at n = 0 we get a(φ 0) = 0 — forcing the first subsequence term to be zero. GPT uses range (n + 1) to avoid this. A classic off-by-one that Lean's type system is designed to catch, but the statement must be right first.
theorem polya_szego_104 {α : Type*} [NormedAddCommGroup α] [CompleteSpace α]
(u : ℕ → α) (hu : ∃ l : α, Tendsto u atTop (𝓝 l)) :
∃ (φ : ℕ → ℕ) (s : ℕ → α), StrictMono φ ∧
(∀ n, s n = ∑ k in Finset.range (φ n), u k) ∧
Summable (fun n => ‖s n‖) := by
sorryThe bug: Confuses subsequence values with partial sums of the original sequence. The problem says the subsequence terms are partial sums of a new absolutely convergent series a — not sums of u itself. Also claims Summable (‖s n‖) (the partial sums are summable in norm), which is not what "absolutely convergent series" means.
theorem polya_szego_1_104 (a : ℕ → ℝ) (h : ∃ L, Tendsto a atTop (nhds L)) :
∃ f : ℕ → ℕ, StrictMono f ∧
Summable (fun k ↦ |a (f (k + 1)) - a (f k)|) := by
sorryWhat's clever: Gemini realizes that if the subsequence values are partial sums of an absolutely convergent series, then the consecutive differences a(f(k+1)) - a(f(k)) must be absolutely summable. This is mathematically equivalent — but marked partial because it doesn't explicitly exhibit the series or state the partial-sum relationship.
Assume that
$f(z)$ is analytic, with$w = u + iv = f(z) = f(x + iy)$ . Verify that$$u_x^2 + v_x^2 = u_y^2 + v_y^2$$ (plus follow-up parts about Laplacians, Jacobians, and conformal mappings)
0/6 models get the full problem right.
- Gemini formalizes part 55.1 perfectly but ignores parts 55.2–55.5 → partial
- Claude tries multiple parts but sets the conclusion of 55.1 to
True→ partial - Kimi attempts all parts but uses undefined
∂notation for partial derivatives → wrong - DeepSeek runs out of tokens mid-formalization — code is truncated → wrong
The deeper issue: Lean 4 has no built-in notion of "partial derivative of a complex function viewed as a real-valued function of two real variables." Formalizing the Cauchy-Riemann identity requires decomposing f : ℂ → ℂ into real/imaginary parts as functions ℝ² → ℝ, then relating deriv f to the Jacobian matrix. None of the models find a clean way to do this, even though the mathematics is undergraduate-level.
This is the core finding: the bottleneck is not mathematical understanding but the gap between informal reasoning and formal type theory.
A sequence
$x_1, x_2, x_3, \ldots$ ,$0 \leq x_n \leq 1$ , is equidistributed on$[0,1]$ if and only if the "probability" of a term$x_n$ falling into a certain subinterval of$[0,1]$ is proportional to its length.
0/7 models get this right, even though the text is clean and the mathematics is well-known (Weyl's criterion).
The arbiter flags the most common failure as wrong_type: models define equidistributed using (Finset.card ...) / n, which performs integer division in Lean (since both operands are ℕ). The result is always 0 or 1, making the definition vacuous. The fix requires casting to ℝ before dividing — a one-character change mathematically, but a type-system pitfall that every model falls into.
Of the 317 problems in the experiment:
| Category | Count | % |
|---|---|---|
| Clean | 222 | 70% |
| Corrupted (OCR/mismatch) | 64 | 20% |
| No arbiter evaluation | 31 | 10% |
Corruption types:
- Data mismatch (38 problems): Problem text and book solution describe different problems, likely from OCR page-boundary errors
- Garbled text (18 problems): OCR artifacts rendering the problem unreadable ("Iet smaller than 25 Then", "The ff a constant. W")
- Truncated/empty (8 problems): Problem text too short to be meaningful
When all 7 frontier models fail identically on a problem, the input is almost always broken — not the models. Excluding corrupted data raised success rates by 2–3 percentage points and reduced "all wrong" from 71 to 8 problems.
-
Formalization is hard. The best models get ~38% of clean problems right. For comparison, informal mathematical reasoning on the same corpus is 95%+ accurate.
-
Type precision differentiates models. The most common failures — wrong conclusion, missing hypothesis, wrong type — are about getting Lean types exactly right. Models better at structured output (GPT, Gemini) outperform those optimized for reasoning chains (DeepSeek, MiniMax).
-
Multi-part problems are unsolved. When a single entry contains several sub-statements (e.g., Problem 55.1–55.5), no model reliably formalizes all of them.
-
Off-by-one and type coercion errors are endemic.
Finset.range nvsrange (n+1), integer division vs real division,ℝvsℂ— these are exactly the errors formal verification is designed to catch, but the statement itself must be right first. -
Data quality sets a floor. 20% of problems have corrupted input. Cleaning the OCR pipeline would significantly expand the usable benchmark.
Formalization: Each model receives problem text + book solution and produces a Lean 4 theorem statement with sorry proof. Max tokens: 8192 (16384 for MiniMax). 4 models run concurrently per problem.
Arbiter: Claude Opus 4.6 reads the problem, solution, and all 7 formalizations, then outputs a structured JSON verdict per model: verdict type, confidence, issue categories with severity, and suggested fixes.
Corruption filter: Problems classified as corrupted if (a) all models flagged by arbiter for "completely different problem," (b) problem text is garbled/truncated, or (c) manual inspection confirms unreadable input. Script: classify_corruption.py.
Models: DeepSeek R1 (Novita), GLM-5, Kimi k2, MiniMax (Baseten), GPT-5.4 (OpenAI), Claude Opus 4.6 (Anthropic), Gemini 3.1 Pro (Google).
Data: Arbiter verdicts in arbiter/{n}.json, formalizations in formalizations/{model}/{n}.lean, aggregate stats in summary.json, corruption classification in classification.json.