The AI Mathematical Olympiad Prize

In November 2023, the quantitative trading firm XTX Markets put up US $10,000,000 for a very specific bet: that no publicly-shared AI model could yet solve International Mathematical Olympiad (IMO) problems at gold-medal level. The AI Mathematical Olympiad Prize (AIMO Prize) offers a $5,000,000 grand prize to the first open model that clears that bar, plus up to $5,000,000 in smaller progress prizes along the way, awarded through timed competitions on unseen olympiad-style problems.

The bet matters because language models are notoriously good at sounding right. They can produce a page of confident, beautifully formatted algebra that is subtly, fatally wrong — a wrong turn on line three that cascades into a false conclusion nobody notices unless they check every step. Olympiad geometry, number theory and combinatorics problems are brutal tests for exactly that failure mode: there is no partial credit for vibes, and a single unjustified step invalidates the whole proof.

So AIMO isn't asking "can an AI write something proof-shaped?" It's asking whether a model can produce an integer final answer, under a strict time limit, on problems it has never seen — reasoning that has to survive a much colder kind of scrutiny than a helpful-sounding paragraph.

Here is a genuine olympiad-flavored claim: for every positive integer $n$, the number $n^3 - n$ is always divisible by $6$. Pick any whole number, and the demo will verify the claim by brute force — then walk through the actual proof one step at a time, exactly the way a grader (human or AI) has to check it.

<p class="hint">{{hint_para}}</p>
<div class="row">
  <label for="n-input">{{n_label}}</label>
  <input id="n-input" type="number" min="1" max="999" value="7" />
  <button id="brute" type="button">{{btn_brute}}</button>
  <button id="walk" type="button">{{btn_walk}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div class="status" id="status">{{status_initial}}</div>
<ol id="steps" class="steps"></ol>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.row { display: flex; align-items: center; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
label { font-size: .85rem; font-weight: 600; color: #1d3557; }
input[type="number"] { width: 5.5rem; padding: .35rem .5rem; border: 1px solid #adb1b8;
  border-radius: 6px; font: 600 15px ui-monospace, monospace; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
  background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.status { font-size: 1rem; font-weight: 600; margin: .3rem 0 .6rem; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.steps { margin: 0; padding-left: 1.2rem; font-size: .92rem; line-height: 1.55; }
.steps li { margin-bottom: .4rem; }
.steps li.reveal { animation: fade .25s ease-in; }
@keyframes fade { from { opacity: 0; } to { opacity: 1; } }
code { background: #e8eef3; padding: .05rem .35rem; border-radius: 4px; font: 600 .92em ui-monospace, monospace; }

// Code not found

Notice what each button does. Verify by brute force just computes $n^3-n$ and divides — that's the "guess-and-check" a language model does when it pattern-matches the right final number without reasoning about why. Walk the proof instead builds the argument step by step: factor $n^3-n$, show why one of three consecutive integers is a stepping stone to divisibility by both 2 and 3, and only then declare the claim proven for all $n$, not just the one you tried. Getting the number right is easy. Justifying every step is the actual olympiad.

AIMO is really testing an asymmetry that runs through all of mathematics and computer science.

• Checking a final numeric answer is cheap: plug in the number, compare against ground truth. This is what plain "answer accuracy" leaderboards measure.
• Checking a fully written-out, formal proof is also comparatively cheap — a proof assistant like Lean or Coq can mechanically verify every inference step, because a valid proof is a certificate that a much smaller checker can confirm.
• Generating that proof is the hard part. There is no known efficient recipe for finding the right sequence of algebraic moves, case splits, and clever substitutions — search over possible proofs blows up combinatorially, and in general, deciding whether a mathematical statement is even provable from a set of axioms is undecidable (a consequence of Gödel's incompleteness theorems and the unsolvability of the Entscheidungsproblem).
• This is the same certificate asymmetry that defines P vs NP: a candidate solution — a proof, a satisfying assignment, a short path — is fast to verify but can be brutally slow to find. AIMO forces models to actually do the finding, under a clock, instead of quietly retrieving a memorized final answer.

That is why AIMO's early progress prizes required models to show their work end to end and be graded on the final answer only after real reasoning, not lookup — and why the field is racing toward hybrids that pair a language model's intuition for which step to try with a formal verifier that guarantees the step is actually valid.

"Sounding right" and "being right" diverge everywhere models are asked to reason, and the AIMO Prize is a clean, adversarial testbed for closing that gap:

• Formal verification: proof assistants like Lean, Coq and Isabelle already certify software and hardware correctness; AI that can generate proofs those tools accept could automate huge amounts of that work.
• Scientific discovery: a model that reliably distinguishes a proven conjecture from a merely plausible one is far more trustworthy as a research collaborator.
• Safety-critical reasoning: anywhere an AI's chain of "steps" needs to be independently checkable — legal reasoning, financial models, medical decision support — the checker/finder asymmetry is exactly what determines whether you can trust the output.
• Benchmarking AI progress honestly: AIMO deliberately used unpublished problems so models couldn't have memorized the answers, a template now used across many reasoning benchmarks to separate genuine capability from data contamination.

Progress Prize 1 (2024) was won by Team Numina, whose approach combined large language models with tool use and careful data curation — a preview of how the frontier keeps moving past pure pattern-matching toward checkable reasoning, the same theme running through Gödel's incompleteness theorems and P vs NP.

The AIMO Prize is, on its surface, a competition about integers and geometry problems. Underneath, it's a $10,000,000 stress test of the gap between a model that sounds like it's reasoning and one that actually is — the same gap that separates a lucky guess from a certified proof.

Team Numina's 2024 win proved the gap is closing, not closed. Until the $5,000,000 grand prize is claimed, every attempt is a reminder that in mathematics — as in complexity theory — being convincing and being correct are not the same currency, and no amount of fluency substitutes for a proof that actually checks out.