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