Dirac Achieves a Perfect 6/6 on IMO 2026 at Record Speed · Boundless IntuitionDirac proves 6/6 on IMO 2026→<br>Boundless Intuition’s prover Dirac proves 6/6 on IMO 2026 at record speed→
← Blog·Aug 11, 2026·AnnouncementsResearch
Dirac Achieves a Perfect 6/6 on IMO 2026 at Record Speed<br>Our autonomous prover produced machine-checked proofs of every problem at this year's International Mathematical Olympiad.<br>Boundless Intuition Research·5 min read
Share
Scaling intelligence without scaling trust is a dangerous trajectory. At Boundless Intuition, we are building systems for verified intelligence to address this.<br>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.<br>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.<br>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.<br>Dirac proved all six.<br>Official contest problems: imo-official.org/problems/2026<br>Our verified solutions: github.com/Boundless-Intuition/IMO2026<br>The result<br>All three systems were run against the same formalizations. Total proving time across the six problems:<br>Total proving time<br>Hours to prove all six problems
Fig. 1Total time to prove all six problems. Dirac takes 7h 18m; the other publicly reported results on the same formalizations are shown alongside for reference.SystemAll six provedTotal proving timeVerificationDirac (ours) Yes7h 18m Comparator passPramaana HardyYes8h 57mComparator passAxiom AxiomProverYes24h 56mComparator passFigures for Hardy and AxiomProver are taken from the results published by Pramaana Labs and Axiom Maths, respectively. We thank both Pramaana and Axiom Maths for publishing their results.
Per problem<br>Proving time by problem<br>Hours per problem
Fig. 2Time is not spread evenly across the paper. Q1, Q4 and Q5 are quick for every system; Q2, Q3 and Q6 account for most of Dirac’s total.ProblemDirac timeDirac linesHardy timeHardy linesAxiomProver timeAxiomProver linesQ129m 05s51320m 26s39324m521Q21h 20m 18s1,5722h 53m7386h1,224Q32h 10m 28s2,6973h 04m2,77214h 29m4,229Q415m 59s38716m 20s30739m520Q518m 11s32331m 09s3371h 05m457Q62h 44m 05s7061h 52m3322h 19m771Total 7h 18m 06s 6,198 8h 57m 4,879 24h 56m 7,722<br>Dirac is faster overall and the margin comes from the hard end of the paper rather than from the easy problems.<br>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.<br>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.<br>Cost<br>ProblemCost (USD)Q1$15.18Q2$55.79Q3$29.53Q4$9.55Q5$15.47Q6$51.06Total $176.58<br>Where it got interesting<br>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.<br>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.<br>What comes next<br>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.<br>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.
More from the lab
Announcements · Research · Aug 6, 2026Towards Verified Superintelligence<br>AI is becoming the operating system of the modern world,...