AxiomProver at IMO 2026

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 as sorry, autonomously generated by AxiomProver.
• solution.lean — the verified formal proof, autonomously generated by AxiomProver.

Problems

1. 2026 Q1: [statement] [solution] (521 lines, 24 minutes).
2. 2026 Q2: [statement] [solution] (1224 lines, 360 minutes).
3. 2026 Q3: [statement] [solution] (4229 lines, 869 minutes).
4. 2026 Q4: [statement] [solution] (520 lines, 39 minutes).
5. 2026 Q5: [statement] [solution] (457 lines, 65 minutes).
6. 2026 Q6: [statement] [solution] (771 lines, 139 minutes).

Building

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

Verification

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)

Results have also been validated locally using Comparator.