2026年国际数学奥林匹克竞赛于7月15日至16日在上海举行。中国科学院数学与系统科学研究院开发的数学研究智能体 MechMath Agent Team 解决了全部六道题目并自动实现了形式化。MechMath Agent Team工作流全自动生成题目解答，提供了自然语言证明与对应的形式化版本。相关信息可在项目仓库中获取。

1、问题概述

MechMath Agent Team针对IMO竞赛的6道题目，分别给出了解答：

• • Q1 是一个整数上的数论问题。其解答过程发展了gcd/lcm移动规则，证明了终止性和不变性，并通过素进位数（prime-adic）数据确定了终值。
• • Q2 为欧氏空间中的几何题。证明通过复数坐标表示，在几何约束和代数恒等式之间建立了桥梁。
• • Q3 涉及区间细分上的组合博弈。其推导处理了有序分段长度、交替差异以及确定博弈值所需的下界和上界。该题最终开发形式化代码2,983行，为6道题目中最复杂的一题。
• • Q4 是一道几何博弈题，通过三角形角度和递归定义的必胜位置来表述。
• • Q5 是正实数上的函数不等式。形式化证明首先建立了根式不等式的可靠平方等价形式，然后推导出了函数所需的结构性约束。
• • Q6 回归数论，涉及一个递归定义的数列，使用共享质因数、无平方因子化简（squarefree reductions）和周期性论证。

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

2、结果、验证与时间

    为保证所有证明结果均为模型独立自主生成，我们为所有实验配备了离线沙箱环境，全程关闭网络访问与网页搜索，保证模型无法获取外部解题资料。

对于每道题，我们分别提供了三个文件：

• • problem.lean，包含原问题形式化陈述；
• • solution.lean，包含完整的、经过机器检查的 Lean 证明；
• • solution.pdf，包含面向数学读者的表述。

    MechMath Agent Team产生的完整的形式化证明位于对应的 solution.lean 文件中，且均已通过依赖关系检查：所有文件无任何占位证明语句，通过公理核验指令可溯源全部逻辑依赖，仅使用Lean标准基础公理，无自定义公理与隐性逻辑漏洞。项目基于Lean 4.29.0与配套Mathlib库构建，完整的源代码树和面向读者的 PDF 文件可在项目仓库中浏览。

    实验分别统计了模型生成自然语言证明（NL）与Lean形式化证明（FL）的耗时（如表1所示）。整体来看，几何、组合类题目形式化适配成本更高，需要大量的形式化基础设施。而部分高推理难度题目，在广泛探索确定核心推导范式后，即可快速完成轻量化形式化翻译。

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