2026年国际数学奥林匹克竞赛于7月15日至16日在上海举行。我院开发的数学研究智能体MechMath Agent Team自动解决了全部六道题目并自动实现了形式化。相关信息可在[IMO2026项目仓库](https://github.com/MechMath/IMO2026)中获取。这些解答由MechMath Agent Team工作流生成。以下是关于此项工作的介绍。

一、问题集锦、结果与性能

Q1是一个关于整数棋盘上的数论问题。其形式化过程发展了gcd/lcm移动规则，证明了终止性和不变性，并通过素进位数（prime-adic）数据确定了终值。

Q2 是一道在欧几里得平面中形式化的几何题。证明通过复数坐标表示，在几何约束和代数恒等式之间建立了桥梁。

Q3 涉及区间细分上的组合博弈。其推导处理了有序分段长度、交替差异以及确定博弈值所需的下界和上界。该题形式化开发共2,983行，是本集合中规模最大的。

Q4 是一道几何博弈题，通过三角形角度和递归定义的必胜位置来表述。

Q5 是正实数上的函数不等式。形式化证明首先建立了根式不等式的可靠平方等价形式，然后推导出了函数所需的结构性约束。

Q6 回归数论，涉及一个递归定义的数列，使用共享质因数、无平方因子化简（squarefree reductions）和周期性论证。

以上问题集合为MechMath智能体团队工作流提供了一个紧凑但多样化的测试平台。其题目横跨数论、欧几里得几何、组合数学、博弈论和函数不等式，因此同时测试了数学路径选择与形式化证明的工程实现。

二、结果、验证与时间

对于每道题，成果包含了三个文件：

`problem.lean`，包含形式化陈述；

`solution.lean`，包含完整的、经过机器检查的 Lean 证明；

`solution.pdf`，包含面向数学读者的表述。

`problem.lean`文件按设计保留了 `sorry` 占位符，以便提供简洁的定理接口。完整的证明位于对应的 `solution.lean` 文件中。每个形式化解在其主要定理证明结束时，会打印其所用的公理，使得其逻辑依赖关系在构建完成后可直接检查。完整的源代码树和面向读者的 PDF 文件可在[项目仓库]（https://github.com/MechMath/IMO2026）中浏览。

时间数据如下表所示。NL表示生成自然语言证明的记录时间，FL表示生成形式化证明的记录时间。时间本身并非数学难度或证明质量的衡量标准，但其对比具有参考意义。几何和组合论证可能需要大量的形式化基础设施，而较长的自然语言探索一旦确定了正确的不变量或表示方法，最终可能收敛为一个相对紧凑的形式化证明证书。

表注：表中时间，单位为分钟；数值四舍五入至小数点后两位，数据来源于项目README文件。

该项目使用 Lean 4 和 Mathlib 构建，版本均为4.29.0。标准构建过程会检查 `solution.lean` 文件及其定理依赖关系，而打印出的公理报告则提供了额外的、透明的验证记录。

特别地，针对第二题（几何），额外采用了一种通过中间态语言翻译的方法，以及将大模型和符号计算（计算机代数系统）结合的证明方法，从自然语言题目自动翻译并完成Lean的证明，仅花费68分钟，用328行Lean代码便完成了证明。这一证明器将于近期发布。

关于MechMath Agent Team更多信息，欢迎访问mechmath.github.io