Lean prover Dirac solves the 2026 International Mathematical Olympiad

Boundless Intuition's autonomous proving agent Dirac proved all six problems of the 2026 International Mathematical Olympiad in 7 hours 18 minutes, faster than Pramaana Hardy's 8 hours 57 minutes and Axiom AxiomProver's 24 hours 56 minutes, at a total compute cost of $176.58. The company says the result demonstrates progress toward verified intelligence that can be trusted across mathematical, tax, medical, and other domains.

Scaling intelligence without scaling trust is a dangerous trajectory. At Boundless Intuition, we are building systems for verified intelligence to address this. That requires solving two problems at once. Verification must be rigorous enough to establish correctness and fast enough to be useful in the real world. Eventually, this approach must generalize. The same underlying reasoning system should be able to operate across mathematical theorems, tax rules, medical constraints, semiconductor specifications, security policies, and other domains. The formal representation and verification mechanism may differ, but the need for a checkable guarantee remains the same. The International Mathematical Olympiad is a useful stress test for that ambition. IMO 2026, held in Shanghai on 15–16 July 2026, is the most prestigious mathematics competition in the world, and its problems are hard in ways that expose the weaknesses of automated provers. We ran Dirac , our autonomous proving agent, on the publicly released formalizations of all six problems published by Axiom Maths and compared our results against other externally published provers on the same statements. Dirac proved all six. - Official contest problems: imo-official.org/problems/2026 https://www.imo-official.org/problems/2026/ - Our verified solutions: github.com/Boundless-Intuition/IMO2026 https://github.com/Boundless-Intuition/IMO2026 The result All three systems were run against the same formalizations. Total proving time across the six problems: | System | All six proved | Total proving time | Verification | |---|---|---|---| Dirac ours | Yes | 7h 18m | Comparator pass | | Pramaana Hardy | Yes | 8h 57m | Comparator pass | | Axiom AxiomProver | Yes | 24h 56m | Comparator pass | Figures for Hardy and AxiomProver are taken from the results published by Pramaana Labs https://github.com/pramaana-labs/imo2026-lean and Axiom Maths https://github.com/AxiomMath/IMO2026 , respectively. We thank both Pramaana and Axiom Maths for publishing their results. Per problem | Problem | Dirac time | Dirac lines | Hardy time | Hardy lines | AxiomProver time | AxiomProver lines | |---|---|---|---|---|---|---| | Q1 | 29m 05s | 513 | 20m 26s | 393 | 24m | 521 | | Q2 | 1h 20m 18s | 1,572 | 2h 53m | 738 | 6h | 1,224 | | Q3 | 2h 10m 28s | 2,697 | 3h 04m | 2,772 | 14h 29m | 4,229 | | Q4 | 15m 59s | 387 | 16m 20s | 307 | 39m | 520 | | Q5 | 18m 11s | 323 | 31m 09s | 337 | 1h 05m | 457 | | Q6 | 2h 44m 05s | 706 | 1h 52m | 332 | 2h 19m | 771 | Total | 7h 18m 06s | 6,198 | 8h 57m | 4,879 | 24h 56m | 7,722 | Dirac is faster overall and the margin comes from the hard end of the paper rather than from the easy problems. Q3 is where AxiomProver spent 14h 29m. Dirac cleared it in 2h 10m with a 2,697-line proof, shorter than Hardy’s 2,772 and well under AxiomProver’s 4,229. Q2 is the geometry problem, historically the place where Lean proofs blow up in length and search time. Dirac finished in 1h 20m, against 2h 53m for Hardy and 6h for AxiomProver, by attacking the problem through vectors and linear algebra rather than synthetic geometry. The trade-off is visible in the line count: our proof is more than twice the length of Hardy’s. Cost | Problem | Cost USD | |---|---| | Q1 | $15.18 | | Q2 | $55.79 | | Q3 | $29.53 | | Q4 | $9.55 | | Q5 | $15.47 | | Q6 | $51.06 | Total | $176.58 | Where it got interesting Q3. Dirac split the game into an upper bound and a lower bound, farmed out a large lemma toolkit to parallel sub-tasks, proved a long lower-bound argument, and assembled the pieces. It is our cleanest result of the six: faster and shorter. Q6. Dirac reduced the problem to a single crux lemma almost immediately, then spent roughly an hour stuck on the informal argument behind that crux. It eventually extracted a rigorous prime-bounding approach and formalized it cleanly. It got there, but the detour is why Q6 took 2h 44m and trails both competitors. It is the clearest target for the next iteration. What comes next IMO 2026 is one benchmark, but it gives us a clear way to measure progress. Dirac is currently the fastest among the publicly reported systems we compared against, demonstrating that autonomous formal proving can be both rigorous and fast, while still leaving significant room for improvement. Our next focus is pushing Dirac further on proof decomposition, difficult crux arguments, and proving cost, while improving how quickly and effectively it can generalize its reasoning beyond mathematical formalization.