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">Claim: for every positive integer <code>n</code>, the number <code>n&sup3; − n</code> is always divisible by 6. Pick an <code>n</code>, then either check it by brute force or walk through the real proof.</p>
<div class="row">
  <label for="n-input">n =</label>
  <input id="n-input" type="number" min="1" max="999" value="7" />
  <button id="brute" type="button">Verify by brute force</button>
  <button id="walk" type="button">Walk the proof</button>
  <button id="reset" type="button" class="ghost">Reset</button>
</div>
<div class="status" id="status">Choose a number and pick a button.</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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Claim: n^3 - n is divisible by 6 for every positive integer n.
const input = document.getElementById('n-input');
const statusEl = document.getElementById('status');
const stepsEl = document.getElementById('steps');

function setStatus(t, cls) { statusEl.textContent = t; statusEl.className = 'status ' + cls; }
function clearSteps() { stepsEl.innerHTML = ''; }
function addStep(html) {
  const li = document.createElement('li');
  li.className = 'reveal';
  li.innerHTML = html;
  stepsEl.appendChild(li);
}
function getN() {
  const n = parseInt(input.value, 10);
  return Number.isFinite(n) && n >= 1 ? n : 1;
}

// Brute-force mode: just compute n^3 - n and test divisibility for the chosen n.
function bruteForce() {
  clearSteps();
  const n = getN();
  const value = n * n * n - n;
  const divisible = value % 6 === 0;
  addStep(fmt('Compute: %n%<sup>3</sup> − %n% = <b>%value%</b>.', { n: n, value: value }));
  addStep(fmt(divisible ? '%value% ÷ 6 has no remainder. ✓ True for this n — but a single example never proves the claim for every n.' : '%value% is not a multiple of 6 — check your input.', { value: value }));
  if (divisible) setStatus(fmt('n³ − n is divisible by 6 for n = %n% — but that’s just one data point.', { n: n }), 'ok');
  else setStatus('Something’s off — recheck the arithmetic.', 'bad');
}

// Proof mode: factor the expression and argue divisibility by 2 and by 3 in general, for any n.
function walkProof() {
  clearSteps();
  const n = getN();
  const a = n - 1, b = n, c = n + 1;
  addStep(fmt('Factor: n<sup>3</sup> − n = n(n<sup>2</sup> − 1) = n(n − 1)(n + 1). For n = %n%, that’s the product of three consecutive integers.', { n: n }));
  addStep(fmt('So the three consecutive integers are (%a%)(%b%)(%c%) — always of the form (n − 1)·n·(n + 1), whatever n is.', { a: a, b: b, c: c }));
  addStep('Among any two consecutive integers, one is even. So among (n − 1), n, (n + 1), at least one is a multiple of 2.');
  addStep('Among any three consecutive integers, exactly one is a multiple of 3. So one of (n − 1), n, (n + 1) is divisible by 3.');
  addStep('2 and 3 share no common factor, so having a factor of 2 and a factor of 3 among the same three numbers means the whole product is divisible by 2 × 3 = 6.');
  addStep(fmt('Conclusion: n(n − 1)(n + 1) is divisible by 6 for <b>every</b> positive integer n — not just n = %n%. That’s a proof, not a sample.', { n: n }));
  setStatus('Proved for every n, not just the one you tried.', 'ok');
}

document.getElementById('brute').addEventListener('click', bruteForce);
document.getElementById('walk').addEventListener('click', walkProof);
document.getElementById('reset').addEventListener('click', () => {
  clearSteps();
  setStatus('Choose a number and pick a button.', '');
});

<p class="hint">Claim: for every positive integer <code>n</code>, the number <code>n&sup3; − n</code> is always divisible by 6. Pick an <code>n</code>, then either check it by brute force or walk through the real proof.</p>
<div class="row">
  <label for="n-input">n =</label>
  <input id="n-input" type="number" min="1" max="999" value="7" />
  <button id="brute" type="button">Verify by brute force</button>
  <button id="walk" type="button">Walk the proof</button>
  <button id="reset" type="button" class="ghost">Reset</button>
</div>
<div class="status" id="status">Choose a number and pick a button.</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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Claim: n^3 - n is divisible by 6 for every positive integer n.
const input = document.getElementById('n-input');
const statusEl = document.getElementById('status');
const stepsEl = document.getElementById('steps');

function setStatus(t, cls) { statusEl.textContent = t; statusEl.className = 'status ' + cls; }
function clearSteps() { stepsEl.innerHTML = ''; }
function addStep(html) {
  const li = document.createElement('li');
  li.className = 'reveal';
  li.innerHTML = html;
  stepsEl.appendChild(li);
}
function getN() {
  const n = parseInt(input.value, 10);
  return Number.isFinite(n) && n >= 1 ? n : 1;
}

// Brute-force mode: just compute n^3 - n and test divisibility for the chosen n.
function bruteForce() {
  clearSteps();
  const n = getN();
  const value = n * n * n - n;
  const divisible = value % 6 === 0;
  addStep(fmt('Compute: %n%<sup>3</sup> − %n% = <b>%value%</b>.', { n: n, value: value }));
  addStep(fmt(divisible ? '%value% ÷ 6 has no remainder. ✓ True for this n — but a single example never proves the claim for every n.' : '%value% is not a multiple of 6 — check your input.', { value: value }));
  if (divisible) setStatus(fmt('n³ − n is divisible by 6 for n = %n% — but that’s just one data point.', { n: n }), 'ok');
  else setStatus('Something’s off — recheck the arithmetic.', 'bad');
}

// Proof mode: factor the expression and argue divisibility by 2 and by 3 in general, for any n.
function walkProof() {
  clearSteps();
  const n = getN();
  const a = n - 1, b = n, c = n + 1;
  addStep(fmt('Factor: n<sup>3</sup> − n = n(n<sup>2</sup> − 1) = n(n − 1)(n + 1). For n = %n%, that’s the product of three consecutive integers.', { n: n }));
  addStep(fmt('So the three consecutive integers are (%a%)(%b%)(%c%) — always of the form (n − 1)·n·(n + 1), whatever n is.', { a: a, b: b, c: c }));
  addStep('Among any two consecutive integers, one is even. So among (n − 1), n, (n + 1), at least one is a multiple of 2.');
  addStep('Among any three consecutive integers, exactly one is a multiple of 3. So one of (n − 1), n, (n + 1) is divisible by 3.');
  addStep('2 and 3 share no common factor, so having a factor of 2 and a factor of 3 among the same three numbers means the whole product is divisible by 2 × 3 = 6.');
  addStep(fmt('Conclusion: n(n − 1)(n + 1) is divisible by 6 for <b>every</b> positive integer n — not just n = %n%. That’s a proof, not a sample.', { n: n }));
  setStatus('Proved for every n, not just the one you tried.', 'ok');
}

document.getElementById('brute').addEventListener('click', bruteForce);
document.getElementById('walk').addEventListener('click', walkProof);
document.getElementById('reset').addEventListener('click', () => {
  clearSteps();
  setStatus('Choose a number and pick a button.', '');
});

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.