HOA — Humanize Olympic Agents
Mathematics, physics and quantum information, solved by agents and checked by a proof assistant. No rubric, no grader, no benefit of the doubt: Lean 4 either accepts the proof or it does not.
What it has done
| Result | Written up | |
|---|---|---|
| Lean-Eval | First place, 172 research-level problems | 26-08-18 · 26-07-29 |
| IMO 2026 | Six of six, on two different backends, 3.2× faster than the reported agentic result | 26-07-22 |
| PutnamBench | 670 of 672, and every problem in Putnam 2025 | 26-06-26 |
| IPhO 2026 | 23 of 23 theory subproblems, sorry-free | 26-07-29 |
| QAlg | 36 of 36, blind | 26-07-29 |
| QIT | 37 of 40 end to end, 92.5% | 26-07-29 |
| Physics Cup · SuperChem · HLE | The model / tool / flow comparison | 26-07-08 |
What counts as solved
A problem counts only when the Lean file passes every gate. The worker runs a comparator check on its own output; the reviewer re-verifies independently through the AXLE API, with no access to how the proof was arrived at; and the Lean kernel has to accept the term. Candidates that fail any gate are kept for inspection and are never counted.
Nothing is accepted with a sorry placeholder or an unproved assumption standing in for a step. And because a perfectly checked proof of the wrong statement is a real failure mode, semantic review — does this theorem actually say what the problem said — is counted and reported separately from proof review, rather than folded into one number.
What this is really testing
None of this is a claim that agents are good at mathematics. It is a claim about loops.
The models are the ones everybody has. What differs is the arrangement around them: who works and who reviews, what carries between attempts and what is deliberately forgotten, when a line of attack is abandoned, and how a run of hundreds of hours is kept from going in circles. A formal verifier is the ideal instrument for measuring that, because it removes every way of being approximately right.
The clearest version of the argument is the model / tool / flow table: the same model scores 2 of 50 through the raw API, 18 of 50 through its own CLI, and 50 of 50 inside a flow.
Where the code is
humanfia/imo2026 · humanfia/putnambench-solver · humanfia/flowverse · IPhO 2026 dataset
The loop these runs were built on is Humanize 1. What we learned from watching it run for weeks is most of why RLAR and the rest of the flowverse look the way they do.