IMO 2026 — six of six
A fully agentic run solved all six problems of the 2026 International Mathematical Olympiad. Every solution is machine-checked in Lean 4 against the formal statements published by AxiomMath — there is no rubric and no benefit of the doubt.
What was run
The Humanize 1 flow, in a YOLO-style loop with no human in the turn. Times are API time — the time actually spent inside model calls — which is the only measure that does not reward a slower harness.
| Problem | Humanfia (GPT-5.6) | Humanfia (Kimi-K3) | AxiomProver |
|---|---|---|---|
| Total | 497.7 min | 1,034.9 min | 1,496 min |
| Q1 | 38.1 min | 87.1 min | 24 min |
| Q2 | 100.4 min | 224.3 min | 360 min |
| Q3 | 187.1 min | 343.7 min | 869 min |
| Q4 | 58.7 min | 75.6 min | 39 min |
| Q5 | 46.5 min | 91.9 min | 65 min |
| Q6 | 66.9 min | 212.4 min | 139 min |
The Kimi-K3 run is a hybrid — a Kimi worker paired with a Codex reviewer — and cost $57.70 against the GPT-5.6 run's $127.41. That is the part worth sitting with: two different backends, the same flow, and the cheaper one still closes all six.
Check it yourself
Clone humanfia/imo2026 and run the AXLE verification script against the published Lean solutions. The statements, both sets of solutions and the reproduction scripts are all released.