From 67% to 97%: When Your Theorem Prover Proves the Wrong Theorem

gist_aristotle.md

From 67% to 97%: When Your Theorem Prover Proves the Wrong Theorem

March 2026

---

The Discovery

We evaluated Aristotle — Harmonic's automated Lean 4 theorem prover — on 823 problems from Pólya-Szegő's Problems and Theorems in Analysis. The headline numbers look spectacular:

• 97.6% of problems get a sorry-free, compiler-verified proof
• The system handles combinatorics, analysis, and complex analysis fluently

But when we checked whether Aristotle was proving the right theorem, the picture changed:

• Only 67.3% of formalizations are semantically correct
• ~33% of the time, Aristotle formalizes and proves a different theorem than the one asked for

The proofs are perfect. The theorems are wrong.

Examples

Ternary Weighing (Problem P1_15)

Asked: "Weights 1, 3, 9, 27, ... can weigh any positive integer using both pans, in exactly one way."

Aristotle proved: Existence of a balanced ternary representation — but omitted the uniqueness claim. Half the theorem, fully proved.

Counting Solutions of ax + by = n (Problem P1_26)

Asked: "For coprime a, b, the number of non-negative solutions of ax + by = n equals ⌊n/ab⌋ or ⌊n/ab⌋ + 1."

Aristotle proved: Helper lemmas and a numSolutions definition, but never stated the main theorem connecting it to the floor formula. The code was truncated mid-development.

Bernstein Polynomial Identity (Problem P1_40)

Asked: A specific identity for weighted Bernstein polynomials: ∑(v/n - α)² C(n,v) xᵛ(1-x)ⁿ⁻ᵛ = (x-α)² + x(1-x)/n.

Aristotle produced: Correct auxiliary lemmas and documentation referencing the identity — but never assembled them into a standalone theorem. Mathematically aware, formally incomplete.

Our Fix

We developed an agentic formalization pipeline that catches and corrects this semantic drift. Without modifying Aristotle itself, we achieve:

System	Semantic Accuracy
Aristotle alone	67.3%
Best single LLM (GPT-5.4)	85.2%
Our pipeline	97.4%

On well-posed problems with clean source data, the effective error rate is approximately 2%.

The pipeline produces formalization + proof: a semantically verified Lean 4 theorem statement backed by a compiler-checked proof. Not just a statement with sorry, and not just a proof of the wrong thing.

Generating Function Stress Test

We asked for the generating function identity connecting coin change to power series:

"The number of ways to change N dollars into coins of 1, 5, 10, 25, 50, 100 cents is the coefficient of x^(100N) in the multiplicative inverse of (1-x)(1-x⁵)(1-x¹⁰)(1-x²⁵)(1-x⁵⁰)(1-x¹⁰⁰)"

The pipeline produced a clean formalization in ~20 seconds:

import Mathlib

def usCoinValues : Fin 6 → ℕ := ![1, 5, 10, 25, 50, 100]

def changeWays (N : ℕ) : ℕ :=
  Fintype.card
    {v : Fin 6 → Fin (100 * N + 1) //
      (∑ i : Fin 6, usCoinValues i * (v i : ℕ)) = 100 * N}

def coinDenominator : PowerSeries ℤ :=
  (1 - (PowerSeries.X : PowerSeries ℤ)) *
    (1 - (PowerSeries.X : PowerSeries ℤ) ^ 5) *
    (1 - (PowerSeries.X : PowerSeries ℤ) ^ 10) *
    (1 - (PowerSeries.X : PowerSeries ℤ) ^ 25) *
    (1 - (PowerSeries.X : PowerSeries ℤ) ^ 50) *
    (1 - (PowerSeries.X : PowerSeries ℤ) ^ 100)

theorem changeWays_eq_coeff_coinDenominator_inv (N : ℕ) :
    (changeWays N : ℤ) =
      PowerSeries.coeff ℤ (100 * N) (coinDenominator⁻¹) := by
  sorry

The proof was then generated automatically — a sorry-free, compiler-verified proof including a general lemma about power series coefficients of products of geometric series.

The Irrational Power Test

"Construct two explicit irrational numbers a and b such that a^b is rational."

The classic approach requires either Gelfond-Schneider (hard) or a non-constructive case split (defeats the purpose). Our pipeline found a fully constructive, elementary solution:

def a : ℝ := Real.sqrt 2
def b : ℝ := Real.log 9 / Real.log 2

theorem explicit_irrational_numbers_with_rational_power :
    Irrational a ∧ Irrational b ∧ ∃ q : ℚ, Real.rpow a b = (q : ℝ) := by
  sorry

Here a = √2 and b = log₂ 9, so a^b = 3. Both a and b are irrational by elementary arguments — no Gelfond-Schneider needed.

Try It Yourself

formalize.dimensionreducers.ai — paste any mathematical statement, get a Lean 4 formalization. Click "Formalize + Prove" for a compiler-verified proof.

The Lesson

Proof verification and semantic verification are orthogonal capabilities. A system that compiles 97.6% of its proofs is not a 97.6% reliable system when a third of its theorems are wrong. Compiler-verified proofs of the wrong theorem provide false confidence — they're worse than sorry, because sorry at least announces its incompleteness.

Multi-agent reconciliation bridges this gap. The cost is modest. The accuracy improvement is transformative.

Benchmark

823 problems, 8 models, all evaluations: github.com/igorrivin/polya-szego-benchmark

Full Model Rankings

Model	Semantic Accuracy
Our pipeline	97.4%
GPT-5.4	85.2%
Gemini 3.1 Pro	73.6%
Aristotle	67.3%
Claude Sonnet 4.6	50.8%
Kimi K2.5	32.7%
GLM-5	22.2%
DeepSeek v3	18.5%
MiniMax M2.5	16.1%