菲尔兹奖首次AI验证与数学文化热潮

就在刚刚过去的一周，一个震撼整个数学界的消息传来：人工智能系统Gauss，仅用5天时间就独立完成了维亚佐夫斯卡8维球堆积证明的形式化验证，随后又用一周时间攻克了更复杂的24维情形，生成了超过20万行Lean代码。这是本世纪首次有菲尔兹奖级别的数学成果被AI完整形式化验证，被数学家称为“自动形式化领域的ImageNet时刻”。

Gauss是由初创公司Math, Inc.开发的推理智能体，能将自然语言推理与完全形式化推理相结合。在此次工作中，AI不仅验证了证明的正确性，还自主发现并修正了原论文中的两处细节错误——一处是函数b(t)计算中缺失的负号，另一处是某一定义的缺陷。普林斯顿大学博士后Liam Fowl惊叹道：“这些新成果令人叹为观止，无疑标志着该领域的发展迈出了跨越式的步伐。”

值得注意的是，这一成就建立在人类与AI深度协作的基础上。2024年，大三学生Sidharth Hariharan与维亚佐夫斯卡共同启动了球堆积证明的形式化项目，人类团队耗时近两年编写了约2万行代码和详细的研究蓝图。正是这份蓝图，为Gauss的后续突破铺平了道路。Hariharan坦言：“当Gauss联系我们并告知研究完成时，我们感到无比震惊。但这项技术让我们满怀期待，因为它拥有创造非凡成就、为数学家提供卓越助力的潜力。”

这一里程碑的意义远超技术层面。自1611年开普勒提出球堆积猜想以来，人类用了近400年才完成三维情形的证明，而其形式化验证又耗费了十余年。如今，AI在数天内即可完成高维空间中最复杂证明的验证，并自主纠正人类疏漏。Math, Inc.首席执行官Jesse Han展望道：“这类技术的最终价值，是让数学家摆脱繁琐的机械性工作，全身心投入到他们最擅长的事情中——构建全新的数学世界。”未来，数学研究的范式或将彻底改变：AI成为数学家不可或缺的“思维放大器”，共同探索人类智慧尚未触及的疆域。

国际数学日引爆全国：从跨界解题到数学文化，π Day的N种打开方式

在北京，2026年中小学生“数学节”的开幕式上演了一场别开生面的“跨界提问·少年破局”环节。港口工程师、金融专家、网络安全专家、医生、文保专家依次登台，向全市中小学生征集真实问题的解决思路：“黑客利用‘万能密钥’，至少成功盗取1个重要账号的概率是多少？”“为康熙皇帝学习几何学使用的多面体模型贴金箔，需要准备多大面积的金箔？”这些问题直指真实世界，引导学生的数学学习从“解题”向“解决问题”跨越。基金公司甚至为小学生出题：设计最合理的压岁钱定投计划。市教委副主任吴洁表示：“‘数学节’是培育孩子们数学兴趣、点亮科学思维、涵养创新精神的重要载体。”

在天津，南开大学2026年数学文化节在八里台校区启幕，近千名大中小学生参与其中。数学趣味游园会上，“数趣无穷”“数趣工坊”两大互动区人头攒动，学生们面对数学游戏、趣味手工、模型拼装等项目，或是独自冥思苦想，或是三五成群热烈讨论。“数启新程”数学文化地标漫游则串联起陈省身故居、文中馆、海冰楼等南开园内的数学文化点位，让师生在行走中感受大师的治学精神与学科传承。有学生兴奋地分享：“以前觉得数学枯燥，但这次文化节让我发现，原来数学可以这么有趣和实用。解出题目的那一刻，成就感满满！”

与此同时，国际数学日的声音也传到了梵蒂冈。教宗莱奥十四世通过致函向国际数学日致以问候，称数学家可以成为“世界的希望标志”。这位1977年毕业于维拉诺瓦大学数学专业的教宗，曾在芝加哥担任高中数学与物理教师。他在信函中鼓励数学家关注人工智能时代的算法伦理，并寄语：“成为世界上的希望、真理与善良的先知。”

参考资料

1，AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证
https://www.thepaper.cn/newsDetail_forward_32764878
2, 北京市中小学生“数学节”开幕
https://www.163.com/dy/article/KO27U5MJ051496PC.html
3, 感受数学之美 提升学生素养 南开大学举办2026年数学文化节
http://news.enorth.com.cn/system/2026/03/15/059224996.shtml
4, Mathematicians Can Become “signs of hope for the world,” Pope Leo XIV Says
https://www.aciafrica.org/index.php/news/20663/mathematicians-can-become-signs-of-hope-for-the-world-pope-leo-xiv-says