【文/观察者网专栏作家潘宇】

今年，一场数学竞赛的初步成绩传出圈外，引起了媒体的关注和全社会的讨论。这件事发生后不久，其实还有一个数学竞赛的结果，影响深远，意义重大，但媒体关注度要低得多。那就是2024年国际数学奥林匹克竞赛（I​​MO）。其中的主角还有科技和互联网巨头。谷歌DeepMind的人工智能AlphaProof和AlphaGeometry 2正确回答了6个问题中的4个，首次获得IMO银牌得主。等级。

AlphaProof 解决了 2 道代数问题和 1 道数论问题，其中包括本次 IMO 中最难的问题，只有 5 名参赛者解决了。 AlphaGeometry 2证明了几何问题，而AI未能解决的2个组合问题。每题最多 7 分，总分 42 分。 AI最终得分为28分，每题都是满分，相当于银牌类别的顶级水平，而今年的金牌起跑分数为29分。

这一结果表明人工智能在处理复杂数学推理的能力上取得了显着的飞跃。数学推理是人类认知能力的重要方面，促进科学发现和技术进步。

对于中国来说，这一结果也意味着重大机遇和挑战。

中国人工智能企业在图像识别等一些领域处于领先地位。这是因为人脸识别、物体检测、医学图像分析等多项技术成果已经应用于支付、安防、智慧零售、交通监控、智慧医疗等领域。与人工智能的其他应用领域相比，它们是最先落地的。得益于中国庞大的人口和丰富的应用场景，以及对基础设施项目的政策和资金支持，中国企业可以积累大量的图像数据，进而促进模型训练和算法优化，参与各种国际比赛。领先。

中国下一个可以广泛应用于实际场景的AI领域在哪里？有潜力的肯定包括智能网联汽车、文化体育教育等，这些也是国内企业投资的重点。中国社会历来高度重视教育，家庭对教育投入巨大。学区房、课外辅导、留学费用占据了很多家庭的大部分支出。人工智能对教育的变革将对中国社会产生深远影响。数学作为一门被中国人视为重中之重的基础学科，是我们观察这种影响的另一个窗口。

从计算到证明

尽管数学一直被称为人类心灵的荣耀，但人类利用机器作为数学的辅助手段已有数千年之久。

早在公元前2400年，算盘等工具就已被发明。 17 世纪的科学家和发明家布莱斯·帕斯卡 (Blaise Pascal) 发明了一种早期的机械计算器，一种可以执行简单加法和减法运算的机器。 20世纪60年代，第一台电子计算器问世。早在20世纪70年代和80年代，世界上一些高中和大学考试就开始允许学生使用计算器。自20世纪90年代以来，许多国家的教育系统开始正式使用计算器作为教学工具，并编写了相应的课程。 ，鼓励学生使用计算器进行复杂的运算。

美国的SAT数学考试于1994年首次允许学生使用计算器。目前，世界上许多国家的标准化数学考试，如AP数学考试、SAT、ACT以及国际数学竞赛，都允许考生使用特定类型的计算器。使用计算器可以帮助学生专注于理解数学概念而不是繁琐的计算，这一点已经不再有争议。中国的基础数学教育以严格、系统着称。中国学生在PISA等国际数学评估中表现出色。虽然我们注重学生的计算能力，但我们也不排斥在高考中使用计算器。

人们普遍认为，无论是在日常生活、教学还是科学研究中，机器帮助人类解决数学计算。 MATLAB、Mathematica、Maple等强大的数学计算工具已经是很多人工作中的必备工具，而适合简单数学运算和统计分析的Excel更是受到人们的青睐。在数学证明方面，机器也发挥着越来越重要的作用。这是一个巨大变化的开始。

此次在IMO 2024上，数学家陶哲轩发表演讲，回顾了数学研究从早期计算工具到现代机器学习的范式转变。他讲了很多例子，这里心理观察中心根据自己的理解做一些总结和评论。

第一个例子是一个表。数学领域的许多重要结果首先是通过数论中的表格发现的，许多猜想也是通过大量的表格发现的。表可以理解为数据库，计算机的基本用途之一就是构建这些有用的数据库。例如，许多数学家，包括陶哲轩本人，都使用一个名为“在线整数序列百科全书（OEIS）”的数据库。

第二个例子是科学计算。例如，利用计算机对各种事物进行建模并求解大量的线性方程或偏微分方程几乎是现代科学研究和工程应用的基石，从天气预报到风洞实验，从新材料和药物的开发到期权定价和核反应堆。设计，它的应用无处不在。

另一种类型的科学计算是 SAT 求解器，它可以解决一些逻辑难题（布尔可满足性问题）。其原理是检查大量的布尔变量，找出是否存在对一组变量的赋值使得整个布尔公式为真。通俗地说，比如给你 1000 个陈述，有些是真的，有些是假的，并且给你一些约束、变量和规则，让你证明某些句子的组合在逻辑上是正确的。通过将数学问题（例如毕达哥拉斯三元问题）转换为布尔逻辑问题，SAT 求解器强大的组合求解能力可用于有效地找到整数解。

第三个例子是形式证明协助。四色定理的证明（任何只使用四种颜色的地图都可以将相邻国家涂上不同的颜色）和开普勒猜想（在三维空间中堆叠球体以最大程度地填充空间的最有效方法），都是计算机辅助证明的著名例子。

为了更简洁地形式化复杂的证明过程，数学家开始使用Lean平台。精益用形式化语言表达数学命题，并通过计算机进行验证，从而使每一个推理步骤都能被自动检查。这为数学研究提供了极大的便利，降低了证明复杂定理的错误率。目前，本科数学课程的基本内容，如微积分、群论或拓扑的基本概念等已经正式化，更多数学领域的内容也正在被添加到这个图书馆中。

数学家彼得·舒尔茨（Peter Scholze）试图利用精益来形式化地验证他的先进数学理论。这些理论需要高水平的数学背景和对非常抽象概念的理解，涉及现代代数几何、范畴论、同源代数和拓扑的深入知识。掌握。舒尔茨对他的证明存有疑虑，而且没有人有能力详细检查细节。如果Lean的形式化证明能够成功，就意味着形式数学可以处理现代数学的前沿问题。利用Lean证明费马大定理的项目也已获得资助并启动。

陶哲轩本人致力于通过众包的方式利用精益探索数学。方法是为一个庞大而复杂的证明写出蓝图，将证明分解成数百个小步骤，每个步骤可以单独形式化然后组合，最后将数万行形式化证明转换回人类—— read 为读取版本，最后一步也是由计算机自动生成的。

这样做的好处是证明过程更加开放，让数学家能够更好地分工和合作。每个人处理任务图中他负责的部分，这通常是他擅长解决的部分，而不需要理解整个证明。由于精益可以自动检查，因此可以确保每个人的工作都符合质量标准。另外，遇到修改时，编译器会自动指出相关的地方，而不需要用传统的方式重写整个证明，大大提高了效率。

最后一个例子就是目前很热门的机器学习。