今年有另一场更值得关注的数学竞赛
► 文 观察者网专栏作者潘禺
今年，一场数学竞赛初赛结果的出圈传播，导致了媒体的聚焦和全社会的讨论。而在该事件不久之后，其实还有另外一场数学竞赛的结果，具有深远的影响和重要的意义，在媒体上得到的关注却小得多。那就是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可以自动检查，就能保证每个人的工作达到质量标准。另外，遇到修改，编译器会自动指出关联的地方，不需要像传统的方式重写整个证明，效率大大提高。
最后一个例子就是当下炙手可热的机器学习。
AI的数学能力
ChatGPT这样的大语言模型在简单的算术计算上会犯错，因为模型并不是从基本原理推导出答案，而是根据输入猜测最可能的输出，这种方法有时候并不奏效。GPT-4的研究人员测试了数百道国际数学奥林匹克（IMO）级别的问题，成功率只有1%，只有一个被简化后的特定问题答对了。大型语言模型在生成回答时依赖于训练数据中学习到的模式，尽管训练数据集非常庞大，但它们可能不包含足够的逻辑推理或数学证明的示例。
DeepMind的AlphaProof和AlphaGeometry2这两个更专门的系统，这次的表现就好得多。
AlphaProof是用于形式化数学推理的系统，结合了预训练的语言模型和AlphaZero强化学习算法，也就是之前自学掌握了国际象棋、将棋和围棋的算法。它在Lean中训练自己证明数学陈述，并通过自动将自然语言陈述翻译成形式化的数学语言陈述，创建了一个不同难度的形式化问题库。AlphaProof通过在Lean中搜索可能的证明步骤来生成候选解决方案，然后证明或反驳它们。在IMO比赛前几周内，它证明或反驳了数百万问题进行自我训练，涵盖不同的难度和广泛的数学领域。
AlphaGeometry是一个神经符号系统，由神经语言模型和符号推导引擎组成，它们协同工作以查找复杂几何定理的证明。一个系统提供快速、“直观”的想法，而另一个系统则提供更深思熟虑、更理性的决策。
语言模型擅长识别数据中的一般模式和关系，可以快速预测可能有用的结构，但通常缺乏严格推理或解释其决策的能力。符号推导引擎基于形式逻辑，并使用明确的规则来得出结论，但缓慢而不灵活。语言模型指导符号推导引擎寻找几何问题的可能解决方案，从无限的可能性中预测哪些像点、线或圆这样的新几何结构最有用。如果未找到解决方案，语言模型将添加一个可能有用的结构，为符号引擎开辟新的推导路径。此循环一直持续，直到找到解决方案。
这有点像诺贝尔经济学奖得主丹尼尔·卡尼曼在《思考，快和慢》一书中提出的人类思维的两种系统，快速思考系统是一种快速、直觉式的思维方式，慢速思考系统是一种缓慢、逻辑性强、需要集中注意力的思维方式。
AlphaGeometry2采用的符号引擎比上一代快两个数量级。当遇到新问题时，使用一种新的知识共享机制来实现不同搜索树的高级组合，以解决更复杂的问题。在今年的比赛之前，AlphaGeometry2可以解决过去25年中83%的历史IMO几何问题，而上一代为53%。在今年的IMO2024中，AlphaGeometry2在收到形式化后的问题后，19秒内解决了第4题（下图，要求证明 ∠KIL和∠XPY之和等于180°，AlphaGeometry2提议构造E，即BI上的一个点，使∠AEB=90°）。
训练AlphaGeometry并不是依靠人工的示例，AlphaGeometry首先生成了10亿个几何对象的随机图形，并详尽地推导出每个图形中点和线之间的所有关系，找到每个图形中包含的所有证明，然后逆向工作以找出需要哪些额外的几何结构（如果有）来得出这些证明。数据经过过滤，排除相似示例，产生一个包含1亿个不同难度独特示例的最终训练数据集。有了这么多添加新几何结构而得到证明的例子，AlphaGeometry的语言模型，就能够在遇到奥数几何题时，为添加新结构提出很好的建议。
我们的教育做好准备了吗
教育对个人成长、社会进步和国家发展都至关重要，人工智能对教育的影响已经来临，过去的运作模式和利益结构早晚都将受到冲击。但或许是因为既有格局的根深蒂固，国内对这方面的讨论还不多，但只要想想，同样长期具备垄断性的传媒行业发生了多大变化，就很难忽视这种改变的前景。
人工智能已经深刻改变了媒体，当人们使用TikTok、抖音、今日头条之类的应用获取信息时，算法主导了内容的个性化推荐和分发。这一结果对传媒行业的影响非常明显，报纸、电视台等传统垄断机构无法再占据流量最大的传播渠道。
在教学上，AI同样已经做到了通过分析学生的学习进度、错误模式和知识漏洞，提供个性化的学习路径和习题练习。
比如，KhanAcademy就使用机器学习算法，根据学生的答题记录提供个性化的题目推荐，使学习更具针对性。AI平台ALEKS通过自动化反馈机制帮助学生在练习中获得即时指导，并通过不同题型进一步巩固知识。在线平台DreamBoxLearning提供自适应数学练习系统，学生的进度可以依据他们的实时表现进行调整，确保学习曲线与能力相匹配。
而在解题和题库方面，AI也已经有了不少实际应用。通过AI应用Socratic，学生可以拍摄问题，系统自动识别问题并提供相应的解答提示及详细的解题过程。Edmentum使用AI生成多样化的习题和测验，以帮助教师设计针对性的评估，节省教师设计练习题的时间。
如今，GoogleDeepMind在高难度的竞赛解题上取得突破，意味着对数学这样最重要的基础学科，通过AI的加持，使优质教育资源能充足提供，不再稀缺，技术上的障碍已经基本扫清。
Google正在基于Gemini开发一种自然语言推理系统，这意味着将不需要依赖人类专家将数学问题翻译成形式化的语言进行处理，能与其它AI系统顺利集成。当AI以自然语言解决数学问题后，科教系统的面貌必将改变。
中国教育有三大梦想，因材施教、教育公平和减负。
因材施教的障碍在于，没有尽全力尝试，许多人并不能认知到自己该走哪条路，家长也不愿接受孩子“是骡子还是马”。选择的迷雾加剧了赛道的狭窄，而AI能提供针对性的评估，有效改善个人天赋与才能的识别效率，帮助每个人更早更精准地定位和把握自己的比较优势。无论是利用图像识别技术的体育测评，还是基于机器学习的数学评估，AI会公正地帮助你判断自己。
AI的发展能否带来社会公平，这历来是一个有争议的问题。对于互联网科技公司来说，用户的增加意味着技术成本的摊薄。虽然话不能说绝对，但从过去的经验看，AI提供的教育资源，与别的互联网服务一样，也很可能是往普及方向发展的。这意味着，除了带来因材施教，AI将促进教育公平。
在减负上，AI也能发挥巨大作用。就像计算器对数学考试的影响，导致部分价值不大的计算在教学和考试中被舍弃，而更专注于考察数学思维、概念的理解和运用。AI的影响也有希望进一步优化教学和考试内容，减轻中国学生在某些解题套路上依靠“题海战术”达到“肌肉记忆”的内卷性消耗。
关注数学的人可能都知道今年国内的一些舆情。某竞赛初赛结果的争议彻底出圈了，某数学大师领衔的某书院的争议，则一直在小圈子内流传。但由于涉及到中国教育的金字塔结构和招考录取的指挥棒，后者对家长和学生的影响面其实并不小。
如果把这两件事放在一起看，这都说明了数学竞赛的门槛很高，数学研究的门槛更高，这条道路只适合极少数的人。这背后牵涉的讨论非常复杂，但这个结论大致不差。
为了挑选出这少数人，需要多数人的陪跑。这种陪跑不仅发生在基础教育阶段，很多数学竞赛的获奖者，在因此避开高考，获得了顶级学府的录取后，最终也都没有选择从事数学研究的道路，这也是网上“IMO金牌与菲尔兹奖”的老生常谈了。偏偏数学又是如此重要，社会在一定程度上容忍了投机与内卷的情况，而形成了鼓励“天才少年”的风气。但对每一个个体来说，内卷的代价要独自承受，成长选择的容错率都是有限的，缺少退路的攀登难以长久，“一将功成万骨枯”的情况伤害社会的总体利益，国家努力给教辅降温，阻止家庭为争夺教育资源而“升级军备竞赛”，背后也有这样的考量。
教育是强国之基，教育资源和住宅用地一样，人为制造出稀缺性，也许能够造成短期的产业繁荣，却可能埋下看不见的长久隐患，比如已经被一再讨论的原始创新不足问题。考虑人口结构的变化和高学历人口的规模，和住房一样，中国优质教育资源稀缺的时代终将过去。
目前，还很难说AI提供的充盈教育资源与个性化辅导，能不能动摇中国教育的金字塔结构，也不清楚教育领域的“今日头条”，这样的规则破坏者和秩序颠覆者会在什么时候出现。但最新的AI技术进展，一定会鼓励创业者与投资者摩拳擦掌，技术将又一次走在从业者和政策制定者的前面。