潘禺：今年有另一场更值得关注的数学竞赛
【文/观察者网专栏作者潘禺】
今年，一场数学竞赛初赛结果的出圈传播，导致了媒体的聚焦和全社会的讨论。而在该事件不久之后，其实还有另外一场数学竞赛的结果，具有深远的影响和重要的意义，在媒体上得到的关注却小得多。那就是2024年的国际数学奥林匹克竞赛（IMO），主角中同样有科技互联网巨头的身影，GoogleDeepMind的人工智能AlphaProof和AlphaGeometry2，答对了6道题中的4道，首次达到了IMO银牌获奖者的水平。
AlphaProof解决了2道代数问题和1道数论问题，包括本届IMO中最难的问题，只有5名参赛者解决了这个问题。AlphaGeometry2证明了几何问题，而2个组合问题AI没能解决。每道题最高可得7分，总共最高42分。人工智能的最终得分为28分，在解决的每个问题上都获得了满分，相当于银牌类别的最高水平，因为今年的金牌从29分开始。
这一结果表明，AI处理复杂数学推理能力有了显著飞跃。而数学推理是人类认知能力的一个重要方面，推动了科学发现和技术进步。
对中国来说，这一结果也意味着重大的机遇和挑战。
中国的人工智能企业在一些领域处于领先地位，比如图像识别。这是因为，人脸识别、物体检测、医疗影像分析等许多技术成果，已经应用在支付、安防、智慧零售、交通监控和智能医疗等，相比于AI的其它应用领域，是率先落地的。又得益于中国巨大的人口规模和丰富的应用场景，加上基建项目的政策与资金支持，中国企业能积累大量的图像数据，进而推动了模型的训练和算法的优化，在各类国际比赛中处于领先。
下一个在中国能广泛应用于实际场景的AI领域是哪里呢？有潜力的肯定包括智能网联车和文体教等，这些也是国内企业投入的重点。中国社会历来高度重视教育，家庭在教育上的投入巨大，学区房、课外辅导、留学费用等占到了许多家庭支出的大头。AI对教育的改变，将深刻冲击中国社会，数学这一被中国人视为重中之重的基础学科，又是我们观察这种影响的一个窗口。
从计算到证明
虽然数学一直被称为人类心智的荣耀，但人类使用机器作为数学的辅助，有着几千年的历史。
早在公元前2400年，类似算盘这样的工具就已经被发明。17世纪的科学家和发明家布莱兹·帕斯卡（BlaisePascal）发明了早期的机械计算器，这种机器可以进行简单的加减运算。20世纪60年代，第一台电子计算器问世。早在20世纪70年代到80年代，世界上的部分高中和大学考试就开始允许学生使用计算器，90年代起，许多国家的教育体系开始正式将计算器作为教学工具，并编写了相应的课程，鼓励学生使用计算器进行复杂运算。
美国的SAT数学考试在1994年首次允许学生使用计算器。目前，世界许多国家的标准化数学考试，如AP数学考试、SAT、ACT以及国际数学竞赛，允许考生使用特定类型的计算器。用计算器可以帮助学生专注于数学概念的理解，而非繁琐的计算，这已经没有太大争议。中国的基础数学教育以严格和系统著称，中国学生在PISA这类国际数学评估中的表现十分优异，尽管我们注重学生的计算能力，但也并不在高考中排斥计算器的使用。
机器帮助人类解决数学计算，无论在日常生活、教学还是科研领域，都已经被普遍接受。强大的数学计算工具如MATLAB、Mathematica、Maple已经是许多人工作的必备，适合简单数学运算和统计分析的Excel更是普及。而在数学证明上，目前机器也在发挥越来越大的作用，这正是巨大变革可能产生的开始。
这次在IMO2024，数学家陶哲轩做了一场演讲，回顾了从早期计算工具到现代的机器学习，数学研究的范式转变。他谈到了许多例子，心智观察所在这里结合自己的理解做一些总结和评论。
第一个例子是表格。数学领域的许多重要成果都是通过数论中的表格首次发现的，许多猜想也是通过大量的表格发现的。表格可以理解为数据库，计算机的一个基本用途就是建立这些有用的数据库。比如，很多数学家，包括陶哲轩自己，使用一个叫做“整数序列在线百科全书”（OnlineEncyclopediaofIntegarSequences，OEIS）的数据库。
第二个例子是科学计算。比如用计算机来建模各种事物，求解大量线性方程或偏微分方程，这几乎是现代科学研究和工程应用的基石，从天气预报到风洞实验，从新材料和药物的研发到期权定价、核反应堆设计，其应用无处不在。
另一种科学计算是SAT求解器，可以解决一些逻辑难题（布尔可满足性问题），其原理是通过检查大量的布尔变量，寻找是否存在一组变量的赋值，使得整个布尔公式为真。通俗地说，比如给你1000个陈述，有的是真的，有的是假的，再给你一些限制条件、变量和法则，让你证明某些句子的组合逻辑上是真的。通过把数学问题，比如毕达哥拉斯三元组问题，转换为布尔逻辑问题，利用SAT求解器强大的组合求解能力，能够有效寻找整数解。
第三个例子是形式化证明辅助。四色定理（任一地图只用四种颜色就能让相邻的国家染上不同的颜色）和开普勒猜想（在三维空间中最有效地堆叠球体，以最大限度填充空间）的证明，都是计算机辅助证明的著名例子。
为了更加简洁地形式化复杂的证明过程，数学家开始使用Lean平台，Lean将数学命题用形式化语言表达并通过计算机验证，使得每一个推理步骤都可以自动检查。这为数学研究提供了极大的便利，也降低了证明复杂定理的出错率。目前本科数学课程中的基础内容，比如微积分、群论或拓扑学的基本概念等，都已经被形式化，更多数学领域的内容也在被加入到这个库中。
数学家PeterScholze就利用Lean试图形式化验证自己的高深数学理论，这些理论需要高层次数学背景和对非常抽象的概念的理解，涉及到对现代代数几何、范畴论、同调代数和拓扑学的深入掌握。Scholze对自己的证明存有疑虑，也没有人有本事详细查看其中的细节。Lean的形式化证明如果能够成功，意味着形式化数学能处理现代数学的前沿问题。用Lean证明费马大定理的项目，目前也已经获得资助并启动。
陶哲轩自己则致力于以众包方式来用Lean探索数学。其方法是为大型的复杂证明编写一个蓝图，将证明分解成数百个小步骤，每个步骤都可以单独形式化，然后组合起来，最后将长达数万行的形式化证明转换回人类可读的版本，最后这步也是计算机自动生成的。
这样的好处是，证明过程更加开放，让数学家们可以更好地分工合作，每个人处理任务图中自己负责的部分，通常是自己擅长解决的，而不需要理解整个证明。由于Lean可以自动检查，就能保证每个人的工作达到质量标准。另外，遇到修改，编译器会自动指出关联的地方，不需要像传统的方式重写整个证明，效率大大提高。
最后一个例子就是当下炙手可热的机器学习。