AxiomMath/IMO2026

[](https://axiommath.ai/) # AxiomProver 在 IMO 2026 IMO 2026 是全球最负盛名的大学前数学竞赛，已于 2026 年 7 月 15 日至 16 日在上海举行。AxiomProver 解答了全部六道题目，获得了 42/42 的满分。AxiomProver 是一个用于 Lean 4 的自主多智能体集成定理 证明器，由 [Axiom Math](https://axiommath.ai/) 开发。 本仓库包含了本次竞赛所有六道题目的正式 Lean 4 命题和解答。 题目的官方来源是 https://www.imo-official.org/problems/2026/。 每道题目位于 `IMO2026//` 下： - `problem.lean` — 形式化命题，主体部分留作 `sorry`，由 AxiomProver 自主生成。 - `solution.lean` — 经过验证的形式化证明，由 AxiomProver 自主生成。 ## 题目 1. **2026 Q1**: [[命题]](IMO2026/Q1/problem.lean) [[解答]](IMO2026/Q1/solution.lean) (521 行, 24 分钟)。 2. **2026 Q2**: [[命题]](IMO2026/Q2/problem.lean) [[解答]](IMO2026/Q2/solution.lean) (1224 行, 360 分钟)。 3. **2026 Q3**: [[命题]](IMO2026/Q3/problem.lean) [[解答]](IMO2026/Q3/solution.lean) (4229 行, 869 分钟)。 4. **2026 Q4**: [[命题]](IMO2026/Q4/problem.lean) [[解答]](IMO2026/Q4/solution.lean) (520 行, 39 分钟)。 5. **2026 Q5**: [[命题]](IMO2026/Q5/problem.lean) [[解答]](IMO2026/Q5/solution.lean) (457 行, 65 分钟)。 6. **2026 Q6**: [[命题]](IMO2026/Q6/problem.lean) [[解答]](IMO2026/Q6/solution.lean) (771 行, 139 分钟)。 ## 构建 基于 Mathlib `v4.31.0` 构建（参见 `lean-toolchain`）。 ``` lake exe cache get # fetch the prebuilt Mathlib cache lake build # build all problem/solution libraries ``` ## 验证 可以使用 `verify.py` 来验证每个 `problem.lean` 和 `solution.lean` 是否兼容， 该脚本会调用 [Axle 的 `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) ``` 预计这将非常快地完成，因为结果已由 Axle 缓存。 要绕过此缓存，请在调用时传入 `--no-cache`，这将强制 Axle 重新计算所有内容， 但耗时会更长： ``` 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) ``` 结果也已使用 [Comparator](https://github.com/leanprover/comparator) 在本地进行了验证。