AxiomProver at IMO 2026 (perfect score)

AxiomProver, an autonomous multi-agent theorem prover for Lean 4 developed by Axiom Math, achieved a perfect score of 42/42 at the 2026 International Mathematical Olympiad in Shanghai, solving all six problems. The verified formal proofs are publicly available on GitHub, marking a milestone in AI-driven mathematical reasoning.

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