All six problems of the 2026 International Mathematical Olympiad, solved by a fully agentic, YOLO-style run with no human in the turn, and every solution formally verified by Lean 4. There is no rubric here and no benefit of the doubt: the kernel accepts the proof or it does not.
Two workers were run independently. Both closed all six.
The times
API time — the time actually spent inside model calls, which is the only measure that does not reward a slower harness — against the times reported by AxiomProver on the same statements.
| Problem | Humanfia (GPT-5.6) | Humanfia (Kimi-K3) | AxiomProver |
|---|---|---|---|
| Q1 | 33.6 min | 77.7 min | 24 min |
| Q2 | 96.2 min | 220.2 min | 360 min |
| Q3 | 179.4 min | 338.4 min | 869 min |
| Q4 | 53.3 min | 65.6 min | 39 min |
| Q5 | 42.4 min | 86.7 min | 65 min |
| Q6 | 62.7 min | 209.0 min | 139 min |
| Total | 467.6 min · 3.2× | 997.6 min | 1,496 min |
The shape of that table is the point. On Q1 and Q4 — the two easiest problems — we lose. On Q3, which is the hardest, we win by nearly five times. A loop earns its keep exactly where the work is long enough for the loop to matter, and nowhere else; on a problem a strong model closes in twenty minutes, the arrangement around it is overhead.
What is released
The formal statements, both sets of Lean solutions and the scripts that reproduce the solving process. Pinned to Lean 4.31.0 and Mathlib.