IMO 2026, the world's most prestigious pre-college mathematics competition, was held in Shanghai on July 15–16, 2026. AxiomProver solved all six problems, achieving a perfect score of 42/42. AxiomProver is an autonomous multi-agent ensemble theorem prover for Lean 4, developed by Axiom Math.
This repository contains the formal Lean 4 statements and solutions for all six problems of the competition.
The official source of the problems is https://www.imo-official.org/problems/2026/.
Each problem lives under IMO2026/<code>/
:
problem.lean
— the formal statement, with the bodies left assorry
, autonomously generated by AxiomProver.solution.lean
— the verified formal proof, autonomously generated by AxiomProver.
2026 Q1:[statement][solution](521 lines, 24 minutes).2026 Q2:[statement][solution](1224 lines, 360 minutes).2026 Q3:[statement][solution](4229 lines, 869 minutes).2026 Q4:[statement][solution](520 lines, 39 minutes).2026 Q5:[statement][solution](457 lines, 65 minutes).2026 Q6:[statement][solution](771 lines, 139 minutes).
Built against Mathlib v4.31.0
(see lean-toolchain
).
lake exe cache get # fetch the prebuilt Mathlib cache
lake build # build all problem/solution libraries
One can verify that each problem.lean
and solution.lean
are compatible
using verify.py
, which calls Axle's verify_proof:
python3 verify.py
Q1: okay=True (passed)
Q2: okay=True (passed)
Q3: okay=True (passed)
Q4: okay=True (passed)
Q5: okay=True (passed)
Q6: okay=True (passed)
This is expected to complete very quickly, as the results are cached by Axle.
To bypass this, pass --no-cache
to the call, which will force Axle to recompute everything, at the cost of a slower time:
python3 verify.py --no-cache
Q1: okay=True (passed)
Q2: okay=True (passed)
Q3: okay=True (passed)
Q4: okay=True (passed)
Q5: okay=True (passed)
Q6: okay=True (passed)