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 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 | 672 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 reached; and the Lean kernel has to accept the term. Candidates that fail any gate are kept for inspection and never counted.
Nothing is accepted with a sorry placeholder or an unproved assumption standing in for a step. A perfectly checked proof of the wrong statement is still a failure, so semantic review — does this theorem say what the problem said — is counted and reported separately from proof review.
What this is really testing
None of this claims 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 right 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
These runs were built on Humanize 1. Watching it run for weeks is most of why RLAR and the rest of the flowverse look the way they do.