AI achieving gold-level olympiad math with open, verifiable solutions

Mostly solved as of Sep 2026. At IMO 2026 (Shanghai, July) Huawei's Celia and RedNote's dots-note-3.0 were officially graded 42/42, NVIDIA's open-weight Nemotron 3 Ultra was graded 30/42 (above the 29-point gold cutoff), and Axiom's AxiomProver produced a Lean 4-verified 42/42 without official sign-off. XTX Markets closed the $10M AIMO Prize on 2026-09-16 without awarding the $5M grand prize, saying open-weight models now claim perfect IMO scores and the frontier has moved to research mathematics. What remains open is only the strict combination: a fully open-source system (open checkpoints, data and training) at gold level with Lean-checked proofs. The AIMO Proof Pilot's best fully-open entry scored 29/42 on human grading.

Source: xtxmarkets.com

import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.Fin
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

/-!
# AI achieving gold-level olympiad math with open, verifiable solutions

This is the one problem whose core is fully concrete in Lean. A contest problem
carries a *formal statement* as a `Prop`. A submission claims a set of problems
and must supply, for each claimed problem, a proof of that `Prop` — so the
acceptance predicate below cannot be satisfied without the mathematics actually
being true and proved. Answer-type problems are formalised the same way, as an
equality with the official answer inside `statement`. Scoring is integer
arithmetic: 7 points per fully solved problem, gold at `minPoints` (35 of 42 at
IMO 2025).

Opaque oracle (`Contest`): only the human-judgement parts — that each `statement`
is a faithful formalisation of the official problem (`faithful`), that the run
respected the contest time limit and had no human assistance, and that the proof
artefacts were published. Kernel checking of the proofs is not modelled inside
this file; it is what a verifier does to a proof of `Solved`.

Who must attest: a jury or independent panel signing off the formalisations as
faithful, plus the run conditions (two 4.5-hour sessions, no human input, no
internet); the proof terms themselves are checked by the Lean kernel, which needs
no attestation.

Units: points are the IMO 7-point scale; `problems` is 6 per contest (two papers
of three); `minPoints` is a point total out of 42.

Checked with Lean 4.33.0 / Mathlib using:
  lake env lean <absolute-path-to-this-file>
-/

namespace OpenSpur.Problems.AutomatedOlympiadMath

/-- A contest problem: its formal statement plus the faithfulness attestation. -/
structure Problem where
  /-- Formal statement; for answer problems, an equality with the official answer. -/
  statement : Prop
  /-- The jury certifies this is a faithful formalisation of the official problem. -/
  faithful : Prop

/-- A contest: `n` problems and the run-condition attestations. -/
structure Contest (n : ℕ) where
  problem : Fin n → Problem
  /-- Both papers were produced inside the official time limit. -/
  withinTimeLimit : Prop
  /-- No human assistance, no internet, no problem-specific hand-formalisation. -/
  noHumanAssistance : Prop
  /-- Proof artefacts were published for independent rechecking. -/
  artefactsPublic : Prop

/-- Points per fully solved problem on the IMO scale. -/
def pointsPerProblem : ℕ := 7

/-- Score of a claimed set: 7 points per claimed problem. -/
def score {n : ℕ} (claimed : Finset (Fin n)) : ℕ :=
  pointsPerProblem * claimed.card

/-- The medal bar. -/
structure Thresholds where
  /-- Minimum point total, e.g. 35 of 42 (the IMO 2025 gold cutoff). -/
  minPoints : ℕ

/-- The IMO 2025 gold cutoff. -/
def imo2025GoldCutoff : ℕ := 35

/-- Acceptance predicate. The fourth conjunct is the mathematics: the submission
must prove the formal statement of every claimed problem. -/
def Solved {n : ℕ} (T : Thresholds) (C : Contest n) (claimed : Finset (Fin n)) :
    Prop :=
  C.withinTimeLimit ∧
  C.noHumanAssistance ∧
  C.artefactsPublic ∧
  (∀ i, (C.problem i).faithful) ∧
  (∀ i ∈ claimed, (C.problem i).statement) ∧
  T.minPoints ≤ score claimed

/-- Gold at the IMO 2025 cutoff. -/
def Gold : Thresholds where
  minPoints := imo2025GoldCutoff

/-- Rung `k` demands `7 * k` points, i.e. `k` fully solved problems: rung 5 is
gold-equivalent on a 6-problem paper, rung 6 is a perfect score. -/
def Rung (k : ℕ) : Thresholds where
  minPoints := pointsPerProblem * k

/-- The point bar tightens monotonically along the rungs. -/
theorem rung_points_mono {j k : ℕ} (h : j ≤ k) :
    (Rung j).minPoints ≤ (Rung k).minPoints := by
  simp only [Rung]
  exact Nat.mul_le_mul_left pointsPerProblem h

/-- Solving a higher rung implies solving every lower rung. -/
theorem solved_rung_mono {n j k : ℕ} (h : j ≤ k) (C : Contest n)
    (claimed : Finset (Fin n)) :
    Solved (Rung k) C claimed → Solved (Rung j) C claimed := by
  intro hs
  obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hs
  exact ⟨h1, h2, h3, h4, h5, le_trans (rung_points_mono h) h6⟩

/-- Claiming more problems can only raise the score. -/
theorem score_mono {n : ℕ} {a b : Finset (Fin n)} (h : a ⊆ b) :
    score a ≤ score b :=
  Nat.mul_le_mul_left pointsPerProblem (Finset.card_le_card h)

/-- A worked instance of the shape a board pays on: a one-problem contest whose
statement is genuinely proved here, with no `sorry`. -/
example : Solved { minPoints := 7 }
    { problem := fun _ => { statement := ∀ n : ℕ, Even (n * (n + 1))
                          , faithful := True }
    , withinTimeLimit := True
    , noHumanAssistance := True
    , artefactsPublic := True } (Finset.univ : Finset (Fin 1)) := by
  refine ⟨trivial, trivial, trivial, fun _ => trivial, ?_, ?_⟩
  · intro i _ n
    exact Nat.even_mul_succ_self n
  · simp [score, pointsPerProblem]

end OpenSpur.Problems.AutomatedOlympiadMath

• AIMO Progress Prize 3 (Kaggle)
• AIMO Proof Pilot winners (fully-open models, human-graded proofs)
• Harmonic Aristotle: IMO-level automated theorem proving (arXiv 2510.01346)
• Google DeepMind Gemini Deep Think official IMO 2025 gold (35/42)
• IMO 2026 AI results roundup (official vs self-administered)
• Mathlib (Lean 4 math library used for formal verification)