最年轻菲尔兹奖得主：我用计算机辅助证明研究“大一统”理论
<p style="margin:20px 0px">大名鼎鼎的青年天才数学家，菲尔兹奖得主<strong>彼得 · 舒尔茨</strong>最近发了一个博客，宣告他半年前自己提出的一个挑战，已经成功证明出来了。</p><p style="margin:20px 0px">这项证明是他在 " 大一统 " 数学理论上前进的一大步。</p><p style="margin:20px 0px">神奇的是，他居然是在计算机的帮助下解决的问题。</p><p style="margin:20px 0px">这项研究也证明了计算机可以帮助解决常规性数学难题，一下子吸引了数学圈很多人的关注。</p><p style="margin:20px 0px">主要还是舒尔茨的光芒太过耀眼。</p><p style="margin:20px 0px">毕竟才 32 岁，舒尔茨就已经拿遍了数学界除了阿贝尔和沃尔夫奖之外的所有大奖，还创造菲尔兹奖获奖的最低年龄纪录。</p><p style="margin:20px 0px">据说舒尔茨的爸爸是物理学家，妈妈计算机科学家，姐姐是化学家，再加上他自己是数学家，简直就是涵盖了自然科学领域。</p><p style="margin:20px 0px">而这次用计算机解决数学难题，又再次告诉我们<strong>" 万物皆可 CS"</strong>的道路，不知道是不是他妈妈给他的灵感。</p><p style="margin:20px 0px">让我们来看看这件事的来龙去脉是怎么回事？</p><p style="margin:20px 0px">什么是 " 大一统 " 数学理论</p><p style="margin:20px 0px">数学家们很早之前就开始研究大一统理论了。</p><p style="margin:20px 0px">说到 " 大一统 " 数学理论，不得不提到普林斯顿的<strong>罗伯特 · 郎兰特</strong>这位老爷爷。</p><p style="margin:20px 0px">朗兰兹认为，即使数学中没有关系的分支也可能是相关的。</p><p style="margin:20px 0px">因此，朗兰兹提出了指引数学界发展的伟大构想——<strong>朗兰兹纲领</strong>：</p><p style="margin:20px 0px">数论、代数几何和群表示论这三个相对独立发展起来的数学分支，实际上是密切相关的，而正是一些特别的函数使这些数学分支联系在一起。</p><p style="margin:20px 0px">朗兰兹纲领堪称实现数学大一统的宏伟蓝图，而舒尔茨则被认为是最可能实现这一伟大目标的人。</p><p style="margin:20px 0px">舒尔茨发现：</p><p style="margin:20px 0px">对于几何、泛函分析和 P 进数这三个领域的大一统相当困难，因为它们之间并不兼容。</p><p style="margin:20px 0px">于是，他和哥本哈根大学的 <strong>达斯汀 · 克劳森</strong> 2019 年共同推出了一个 " 凝聚态数学 "（condensed mathematics）的计划。</p><p style="margin:20px 0px">主要目的就是想要实现从几何到数论的各个领域的统一。</p><p style="margin:20px 0px">舒尔茨和克劳森的说：</p><p style="margin:20px 0px">凝聚态数学的关键点是重新定义拓扑的概念，这是现代数学的基石之一。</p><p style="margin:20px 0px">数学家研究的许多物体都有拓扑结构，拓扑提供了一种形状概念，但它比我们熟悉的几何形状更具有延展性。</p><p style="margin:20px 0px">几何、泛函分析和 p 进数这些领域中的每一个领域的，尽管它们显然涉及完全不同的概念许多结果似乎在其他领域都有类似之处。</p><p style="margin:20px 0px">但是，一旦以 " 正确 " 的方式定义了拓扑，这两位研究人员提出，理论之间的类比就会被揭示为同一个 " 浓缩数学 " 的实例。克劳森说，" 这是三个领域的某种大统一 "。</p><p style="margin:20px 0px">因此，去年 12 月份，舒尔茨提出了一个名为<strong>Liquid Tensor Experiment</strong>的挑战，这是 " 凝聚态数学 " 的计划的重要一步。这个名字是向前卫摇滚乐队 Liquid Tension Experiment 致敬，因为两位数学家都是他们的粉丝。</p><p style="margin:20px 0px">这是舒尔茨提出的 Liquid Tensor Experiment 的的挑战：</p><p style="margin:20px 0px">这个月，舒尔茨说已经使用专用计算机软件在一项核心证明上取得了成功。</p><p style="margin:20px 0px">让我们来看看计算机是怎么帮助 " 大一统 " 数学的证明？</p><p style="margin:20px 0px">计算机怎么帮助 " 大一统 " 数学</p><p style="margin:20px 0px">长期以来，数学家一直使用计算机进行数值计算或处理复杂的公式。</p><p style="margin:20px 0px">最著名的，是 1970 年代的一个四色定理证明：</p><p style="margin:20px 0px">任何地图都可以只用四种不同的颜色，就可以在一张地图上填涂任何两个相邻的国家。</p><p style="margin:20px 0px">很明显，计算机可以证明一些逻辑分析，并进行数值计算。</p><p style="margin:20px 0px">但问题是：计算机能处理更复杂的数学吗？</p><p style="margin:20px 0px">为了帮助研究这项工作，舒尔茨和克劳森找来了帝国理工学院的数学家<strong>凯文 · 布扎德</strong>帮忙，他可是<strong>Lean</strong>方面的专家。</p><p style="margin:20px 0px">Lean 是由华盛顿雷德蒙德微软研究院的计算机科学家发明的系统，起初目的是检查计算机代码中的错误。</p><p style="margin:20px 0px">布扎德则根据 Lean 的库中已有的简单的陈述和概念，输入数学陈述，输出复杂的网络。</p><p style="margin:20px 0px">根据研究团队要处理的问题，他们将这些陈述用颜色编码并按数学子领域分组。</p><p style="margin:20px 0px">效果怎么样？</p><p style="margin:20px 0px">随着这个项目的推广，有十几位精通 Lean 的数学家先后加入了进来，实现了在线协作。</p><p style="margin:20px 0px">研究团队的 Lean 版本包含数万行代码，比原始版本长了 100 倍。</p><p style="margin:20px 0px">舒尔茨表示：</p><p style="margin:20px 0px">证明定理 9.4 是挑战的核心，也是我唯一担心的结果。</p><p style="margin:20px 0px">因此，有了它的验证，我对主证明的正确性就没有怀疑了，这个挑战也算完成了一半。</p><p style="margin:20px 0px">请注意，定理 9.4 从任何实际的凝聚数学中抽象出来，所以剩下的一半将涉及大量的形式化的东西，如凝聚的非线性群，非线性范畴中的 Ext 群，以及周围的机器。</p><p style="margin:20px 0px">六个月前，他们只能说 99.9% 确定证明是正确的。</p><p style="margin:20px 0px">但 99.9% 毕竟不是 100%，现在定理 9.4 证明了，他们才 100% 确定结果是正确的了。</p><p style="margin:20px 0px">这个过程实际上是将证明直接输入到 Lean 中。</p><p style="margin:20px 0px">而 Lean 实际上为用户提供了针对目标的非常清晰的步骤，可以用路线图表达。</p><p style="margin:20px 0px">研究团队证明定理 9.4 的路线图如下图所示，绿色表示结果已在 Lean 中得到验证，全部都是绿色表示定理 9.4 已经完全得到验证。</p><p style="margin:20px 0px">研究人员：数学家不太可能很快被机器取代</p><p style="margin:20px 0px">结果很惊喜，但许多研究人员都表示，数学家不太可能很快被机器取代。</p><p style="margin:20px 0px">布扎德就说：</p><p style="margin:20px 0px">计算机无法阅读数学教科书，它们需要人类的持续输入，而且它们无法决定数学陈述是否有趣或深刻——只能决定它是否正确。</p><p style="margin:20px 0px">不过，他补充说，计算机因为运算速度快，能预测数学家看不到的的已知事实的结果。</p><p style="margin:20px 0px">很多网友对这项研究都表示很感兴趣。</p><p style="margin:20px 0px">有网友表示：</p><p style="margin:20px 0px">计算机不会自动完成证明。计算机只是用来验证一个已经存在的证明，所以计算机程序受限于人类数学家的水平。</p><p style="margin:20px 0px">还有网友表示了担忧：</p><p style="margin:20px 0px">计算机的辅助证明可以创造一些关于数学本质的有趣问题，就像厄多斯说 " 你不需要相信上帝，但你需要相信书 "，我不介意将计算机辅助证明作为获得数学新发现的一种方式，但我担心数学正在朝着一个方向发展，即它更多地变成解释学，而不是真正的数学。</p><p style="margin:20px 0px">目前看来，计算机和数学家谁更强还真是一个未知数，未来是怎么样的发展走向也还真不好说。</p><p style="margin:20px 0px">哈哈，抱着吃瓜的心态，真想看看：</p><p style="margin:20px 0px">计算机和人，究竟谁会先证明出 " 大一统 " 理论？</p><p style="margin:20px 0px">团队介绍</p><p style="margin:20px 0px"><strong>彼得 · 舒尔茨</strong></p><p style="margin:20px 0px">德国波恩大学数学学院教授，2018 年菲尔兹奖得主。</p><p style="margin:20px 0px">当前算术代数几何方向无可争议的第一人，是多年来罕见的数学天才。</p><p style="margin:20px 0px"><strong>达斯汀 · 克劳森</strong></p><p style="margin:20px 0px">哥本哈根大学几何和拓扑中心的副教授。</p><p style="margin:20px 0px">在麻省理工学院 Jacob Lurie 的指导下获得博士学位，主要研究代数 K 理论，数论。</p><p style="margin:20px 0px">参考链接：</p><p style="margin:20px 0px"> [ 1 ] https://www.nature.com/articles/d41586-021-01627-2</p><p style="margin:20px 0px"> [ 2 ] https://www.reddit.com/r/math/comments/o3caqq/mathematicians_welcome_computerassisted_proof_in/</p><p style="margin:20px 0px"> [ 3 ] https://news.ycombinator.com/item?id=27559917</p><p style="margin:20px 0px"> [ 4 ] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/</p><p style="margin:20px 0px"> [ 5 ] https://3quarksdaily.com/3quarksdaily/2021/06/the-liquid-tensor-experiment-and-the-rise-of-the-digital-homunculus.html</p><br>免责声明：如果本文章内容侵犯了您的权益，请联系我们，我们会及时处理，谢谢合作！
页:
[1]