为什么值得关注

它是首个在全球最负盛名的中学数学竞赛中获得满分的 AI 定理证明器，所有形式化陈述和证明均由系统自主生成并通过验证。

适合谁使用

自动定理证明和人工智能领域的研究人员
Lean 4 用户和形式化验证从业者
对竞赛题目形式化感兴趣的数学家
数学奥林匹克竞赛的参与者和组织者

典型使用场景

形式化并验证竞赛级别数学问题的解答
在真实问题上对自动定理证明器进行基准测试
研究用于形式化证明生成的多智能体集成方法
构建 Lean 4 中奥林匹克题解的已验证库

项目优势

在 IMO 2026 所有六道题目上获得满分 42/42
自主生成问题陈述和完整证明
所有证明通过 Axle 的 verify_proof 验证并在本地确认
多智能体集成架构能够处理复杂问题（最多 4229 行）

使用前须知

部分问题需要大量计算时间（例如 Q3 耗时 869 分钟）
依赖 Axle 外部验证服务和 Mathlib v4.31.0
需要熟悉 Lean 4 和 mathlib 才能理解与复用

README 快速开始

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//:

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

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

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: ok

IMO2026