# AxiomProver at IMO 2026 (perfect score)

> Source: <https://github.com/AxiomMath/IMO2026>
> Published: 2026-07-17 09:53:29+00:00

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](https://axiommath.ai/).

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/](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.

**2026 Q1**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q1/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q1/solution.lean)(521 lines, 24 minutes).**2026 Q2**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q2/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q2/solution.lean)(1224 lines, 360 minutes).**2026 Q3**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q3/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q3/solution.lean)(4229 lines, 869 minutes).**2026 Q4**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q4/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q4/solution.lean)(520 lines, 39 minutes).**2026 Q5**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q5/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q5/solution.lean)(457 lines, 65 minutes).**2026 Q6**:[[statement]](/AxiomMath/IMO2026/blob/main/IMO2026/Q6/problem.lean)[[solution]](/AxiomMath/IMO2026/blob/main/IMO2026/Q6/solution.lean)(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](https://axle.axiommath.ai/):

```
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)
```