数学家心声：《迈向一个数学公域的世界》by 库纳尔・马尔瓦哈（Kunal Marwaha）2026-10-23
作者：Kunal Marwaha（库纳尔・马尔瓦哈，芝加哥大学博士生）
芝加哥大学量子计算研究生，导师是比尔·费弗曼。他专注于量子算法和量子复杂性理论，之前做过软件工程师，现在还做很多在线兴趣项目 https://kunalmarwaha.com/projects 。
日期：2026-10-5
数学是兼具创造性与情感投入的事业。我们受难题与好奇心驱动；我们审慎地表达想法，以求被精准理解。那些高光时刻会带给我们极致的振奋与震撼。
但从事数学研究的方式一直在演变。我们早已脱离依赖直观图示与非严格论证的阶段，建立起公理与证明体系；也早已告别单人通晓全部已知数学的时代 —— 如今我们走向细分，依靠同行传授自己不熟悉的知识。
如今，数学显然又一次迎来剧变，它的生长速度已经超出人类自身的承载能力。机器已经能够证明全新的数学命题，并整理成论文供人类核验。这很陌生，也冲击着我们现有的研究范式。但在此，我想提出一个积极愿景：接纳这类机器，同时守住我们热爱数学的初心。
我们应当转变思路：不再仅仅做数学前沿的探索者，而要成为世界数学公域（world mathematical commons）的管护者。
公域，指面向全体社会成员开放的公共资源，它能提升所有人的生活品质。我最喜欢的例子是美国国家公园体系。走进国家公园，你总能沉浸于山川、森林、河流带来的磅礴自然之美。你可以露营、游泳，或是仅仅沿着步道漫步。周末出行归来，你带着焕然一新的状态与灵感回归日常。
我喜爱户外，但不算冒险爱好者。而我认识的一些人，把旷野当成归宿。他们会一连数周、数月置身自然：背包徒步、攀岩、记录见闻。有人以此为职业，比如公园护林员、森林防火员；这份工作的报酬，是让他们去认识野生动植物，维系人与自然的平衡，修建步道，方便像我这样的访客享受自然。
我们也可以为数学搭建这样一片园地。
对我们当中很多人而言，研究与其说是一份工作，不如说是热忱所在。这片 “数学旷野” 就是我们的归宿。这也是自动定理证明机器令人心生畏惧的原因：它们是陌生的新存在。我认为这类机器必然会留下来，而且我们无法控制它们会攻克哪些难题。与之相对，我们应当向机器学习，让它和人类理解维持平衡，向更多人展现这片园地的美。我们可以成为数学园地的护林员与防火员 —— 这片数学天地，正比以往任何时候都更富有生机。
自动定理证明机器的突然出现，会让接下来数年充满阵痛与艰难。但如果我们不主动行动，人类研究者很快就会失去自身价值，我们的学术社群也很可能走向凋零。正因如此，搭建数学公域已是迫在眉睫。那么，搭建这个公域需要做些什么？
最关键的一步，是集结一批数学家，共同管护这片公域。我们应当成立一家非营利机构，设立庞大的顾问委员会，代表所有从事定理证明、数学教学从业者广泛多元的诉求。这个组织不能由任何 AI 公司掌控，我们产出的成果应当对所有人开放。
下一步，把全部数学内容转化为形式化可核验命题。这也是 MapMath（数学自动形式化项目 Mathematics Autoformalization Project）的目标 https://www.mapmath.org 。如果能用计算机代码认证证明的正确性，我们就可以大规模维持对这些证明的信任。当下最主流的数学形式化工具是 Lean 证明助手。mathlib4 开源社区活力旺盛，几乎完成了全部本科数学内容的形式化核验。现在甚至可以用大模型直接把前沿研究级别的证明转换成 Lean 代码。（最近费马大定理的形式化工作，就用到了我参与搭建的公开网站 prove2.me 。）
把全部数学形式化之后，会形成一张巨大有向图，记录所有已知命题及其推导关系。只要 AI 企业为公域贡献一部分算力，构建这张知识图谱是可行的。各方可以在此合作，而非相互竞争。未来所有新成果，都可以接入这个知识网络。
最后一步，驯化这张形式化命题图谱。我们不需要一次性消化全部内容，只需要做好管理。我们对图谱做聚类、稀疏化处理，拆解成适合人类认知规模的知识单元。我们从中寻找简化方案、通用定义与统一理论。沿着优美的证明开辟 “步道”，分享给同行，也分享给 “公园访客”（普通爱好者）。机器可以辅助完成所有这些工作，前提是服务于我们的目标。
如果这件事做好了，数学公域将迎来人类理解的黄金时代。依托负责任的管护机制，我们可以和定理证明机器一道培育新一代数学家，在这个充满不确定性的时代，引导数学的演化方向。
一切从组建这个广泛的数学家共同体开始。欢迎加入我们的 Zulip 聊天室，一起讨论搭建数学公域的后续计划。如果你认识能够为数学美好未来出力的人，欢迎把本文转发给他。期待和各位携手同行。
精选评论
评论1 作者：Wen Yang
我非常喜爱这个世界数学公域的构想！我相信 Mathlib 将会是 “数学 2.0” 的重要组成部分。希望这套开放、多元的生态，能够让数学对所有人都更加友好、易于接触。
评论2 作者：M. Winter
我也一直在思考相关问题：
最后一步，驯化这套经过形式化核验的命题图谱。我们不必一次性全盘消化，只需要做好管理。我们应当对图谱做聚类、稀疏化处理，拆解成适配人类认知规模的知识单元。
AI 把数学（乃至更广领域）当中这个庞大的知识管理难题赤裸裸摆到了台面上。我十分推崇维基百科，它把人类知识拆解成一篇篇文章，变成便于驾驭的知识块。我坚信，这套模式有潜力成为知识组织的持久范式—— 可以比作人类知识空间上的一个 ε‑网。
但我要提醒：不宜过度看重 “可核验命题”。数学当中大量有价值的东西，并不是可以形式化、可机器校验的命题。比如巧妙的技巧、直觉感悟、问题本身、定义、叙事、讨论、史实，甚至是有错但富有启发性的证明。
评论3 作者：tchow8
谈及 “把全部数学做形式化” 这个话题，非常推荐阅读《如何形式化全部数学》（xenaproject 博客文章 https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/ ）。引用其中一段话：
如果实施得当，大规模协同形式化工作能够极大拓展数学的探索与发现。倘若做得糟糕，往轻了说是资源浪费；更有可能，会造成长久的伤害。
参考资料
https://proofsandprompts.com/2026/10/23/towards-a-world-mathematical-commons/
https://prove2.me
https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/
形式化证明冷思考：数学证明中的对应问题——by 西蒙・德迪奥（Simon DeDeo）、伊蒙・杜德（Eamon Duede）
AI人工智能正在改变我们撰写形式化证明的方式——莱昂纳多・德・莫拉（Leonardo de Moura）
2026.5数学未来研讨会系列——球体堆积问题的形式化by 玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022年菲尔兹奖得主）——斯坦福FMS
AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum
原标题：《数学家心声：《迈向一个数学公域的世界》by 库纳尔・马尔瓦哈（Kunal Marwaha）2026-10-23》