Research

Are AI Proofs Messier Than Human Proofs?
Esben Kran and Tanya Bas ·

On Tuesday, OpenAI released 719 math manuscripts written by an internal model1. Some of them solve problems that had been open for decades. Yesterday morning, Tanya and I talked about what this means for the elegance of mathematics.

Great proofs stay elegant. But does AI write proofs the way it writes code? It gets the job done, but sometimes in a messy way, because mess is cheap. And if real proofs turn out to rest on mess, maybe Occam’s razor is a fact about human understanding, not about the rules of mathematics.

AI may reach proofs that humans never could, and many of them by brute force. If so, it should pull the distribution of elegance towards messy. We decided to use the messiness itself as the measure: define elegance, score human and AI proofs, and see which way the distribution moves. So we did.

Are AI proofs messier than human proofs?

TLDR; Only a little, and only in the tail. On a 1–10 elegance scale, AI proofs score 6.3 and celebrated human proofs score 6.7, a gap well inside the noise. But 1 in 4 AI proofs lands in the “idea buried under cases and estimates” range, against 1 in 12 human proofs. And the AI proofs score higher on bringing ideas in from other fields.

One dot per proof (click to open the paper): 36 AI proofs (OpenAI, 2026) and 36 human proofs (2018–23) of named open problems, matched by field. Mean of two blind judges (Claude Opus, Gemini 3.1 Pro). Top row: 12 textbook proofs for calibration.

What is elegance?

Mathematicians have tried to define it for a century. Hardy asked for “unexpectedness, combined with inevitability and economy”, and called the enumeration of cases “one of the duller forms of mathematical argument”2. Rota said a proof is beautiful when it is enlightening3. When Inglis and Aberdein asked about 250 mathematicians to rate proofs on 80 adjectives, beauty and intricacy came out as separate factors, and “beautiful” barely correlated with “simple”4. Hilbert even planned a 24th problem on how to measure the simplicity of proofs. Nobody has solved it5.

So I turned the literature into a rubric with five parts: economy relative to the result, a surprising key idea, explanatory power, simple structure, and concept over computation. A sixth part, cross-field unification, is scored separately, because Tao lists it as a different kind of good mathematics6.

The setup

  • AI proofs: 36 results from the OpenAI release that resolve a named problem, and whose main theorem is checked in Lean.
  • Human proofs: 36 papers from 2018–2023 (before AI help) that resolve a named problem, matched by field. Each one is refereed and cited, with no erratum, and an outside source calls it solved. This removed several famous papers, including two with Annals errata.
  • Blinding: the main theorem and its proof are extracted from the LaTeX, with names, dates and AI markers removed.
  • Judges: Claude Opus and Gemini 3.1 Pro score each proof on its own. No GPT, because the AI proofs came from OpenAI.
  • Calibration: six “book proofs” (Furstenberg’s primes, Huang’s sensitivity proof) and six famous brute-force proofs (four colour, Kepler, a 200 TB SAT proof). The judges put every book proof at 9.5 or above and every brute-force proof at 2.75 or below.

What we found

The AI proofs are not messier on average. The difference is −0.4 points (95% CI −1.2 to +0.4), and it stays within the noise when you compare inside each field or control for proof length.

The difference is in the tail, though even that is not significant on 36 proofs per side (p = 0.11). The messy AI proofs grind: a counterexample to Hadwiger’s conjecture built from “peeling, pinning, phase alternatives, compactness limits and parameter ledgers”, in Claude’s words. The messy human proofs are of another kind: Keller’s conjecture by SAT solver and Brauer’s height zero conjecture on top of the classification of finite simple groups. Humans outsource the mess to machines. The AI writes it out.

The best AI proofs are elegant. The top one, the asymptotic Gotsman–Linial conjecture, scores 9.0, next to Hedetniemi’s counterexample (9.25) and Marton’s conjecture (8.75) on the human side. And on cross-field unification, AI scores 3.6 against 3.0 for humans. That is the one dimension where the gap clears the noise, though only just (p = 0.03, one of six tests).

So the synthesis holds, but only weakly. The bulk of the AI distribution sits where the human one does, as Tanya expected. The pull towards messy shows up only in the tail, and with 36 proofs per side we cannot yet separate it from noise. The box is open a crack, not wide.

Why to doubt this

  • The judges are LLMs. They separate textbook proofs perfectly, but they are not referees. Claude can tell which proofs are AI (35 of 36) and names the authors of every human paper. Gemini thinks all 72 are human. Gemini sees a smaller gap (−0.3) than Claude (−0.6).
  • The human set is the best of the best. Refereed, cited, no errata. An average human paper would likely score lower.
  • The AI set is unrefereed. Lean checks the main theorem, not the prose we scored.
  • Excerpts. Most proofs are longer than 25,000 characters, so judges see the theorem, the main proof, and the lemmas it uses, with gaps.

Each result took about three hours of ChatGPT Pro compute1. At that price the mess is cheap, and the question shifts from “is it elegant?” to “who turns it into the book proof?” Einstein’s first paper on relativity was not his last. The four colour theorem is 50 years old and its best proof still rests on 633 configurations checked by computer. For the next thousand AI results, someone has to do that cleanup work, or decide it is not worth doing.

If you’re curious

Does any single score differ between AI and human proofs?
Each rubric score on its own. Bars count proofs at each score: human proofs up, AI proofs down. Lines mark the means.

Only one. AI proofs score higher on cross-field unification (3.6 against 3.0, p = 0.03). They score a little lower on simple structure (2.5 against 3.0, p = 0.16), which matches the messier tail in the main figure. On economy, surprise, explanation and computation, the two sides are within 0.2 points of each other.

Can a classifier tell AI math from human math?

From the elegance scores alone, barely. A logistic regression on the six scores gets 68% right, where chance is 50%.

From the words, perfectly. I removed all math and LaTeX and trained a simple word classifier on the prose that is left. It labels 72 of 72 proofs correctly, each one predicted by a model that never saw it.

The tell is “we”. Human mathematicians write “we” 18.5 times per 1,000 words. The AI writes it 2.8 times. “Our”, “note” and “remark” almost never appear in the AI proofs, and “consequently” is 15 times more common. The humans write as a group of people explaining an idea. The AI writes as no one in particular.

From the notation, mostly yes, but that is still a writing habit. I kept only what sits inside math mode and removed obvious typesetting habits, so \le and \leqslant count as the same symbol, and spacing, bracket sizes and fonts are ignored. A classifier still gets 94% right, and 74% from the list of symbols alone. But this measures which symbols the authors reach for. The human proofs decorate their variables (x̃, x̂, x̄) almost four times as often, while the AI writes plain letters with subscripts. That is notation, not mathematics.

From the shape of the argument, still yes, but less. I parsed each full proof into its lemmas and the chain of results behind the main theorem, and measured only structure: how many lemmas, how deep the chain goes, how many statements get their own proof, how many case splits, how many displayed equations, and how many steps each equation chain takes. No symbols and no words. This classifier gets 79% right. The clearest difference: the AI proves 96% of the statements it uses, the humans 75%. Humans state known results and cite them, while the AI tends to prove them again. The AI’s equation chains are also longer, and its proof text is spread more evenly over its lemmas.

How optimized are the proofs? Could they be tightened?

There are two kinds of tightening, and only one can be measured this way.

Cutting bloat. I asked Claude Opus how much of each proof could be cut without losing a step. The answer is about the same for both: 23% of an AI proof and 25% of a human proof (p = 0.14). What gets cut differs. In human papers, it is remarks, background and second proofs of the same lemma. In AI papers, it is textbook arguments written out in full, such as a complete proof of Hall’s marriage theorem inside a proof about Dixmier’s unitarizability problem.

Finding a better idea. I also asked whether a much shorter proof with a different idea probably exists. Claude said yes for 1 of the 72 proofs. As Tanya put it, to see that a proof is not optimal, you have to know how to tighten it. A judge that cannot find the better proof will not report that one exists.

  1. OpenAI, openai/math (6 Oct 2026); Castelvecchi, Nature, 7 Oct 2026. ↩ ↩2

  2. G. H. Hardy, A Mathematician’s Apology (1940), §18. Archive. ↩

  3. G.-C. Rota, “The phenomenology of mathematical beauty”, Synthese 1997. ↩

  4. Inglis and Aberdein, “Beauty is not simplicity”, Philosophia Mathematica 2015. ↩

  5. R. Thiele, “Hilbert’s twenty-fourth problem”, American Mathematical Monthly 2003. ↩

  6. T. Tao, “What is good mathematics?”, Bull. AMS 2007. ↩

How to cite this work

Esben Kran and Tanya Bas. “Are AI Proofs Messier Than Human Proofs?.” Kran Research, 2026. https://blog.kran.ai/are-ai-proofs-messier 

@misc{kran2026areaiproofsmessier,
  title  = {Are AI Proofs Messier Than Human Proofs?},
  author = {Kran, Esben and Bas, Tanya},
  year   = {2026},
  note   = {Kran Research},
  url    = {https://blog.kran.ai/are-ai-proofs-messier}
}

Discuss Code and data