数学家欢迎“大统一”理论中的计算机辅助证明

彼得森林希望从其基石之一开始重建大部分现代数学。现在，他从一个不太可能的来源获得验证验证他的追求的验证：计算机。

虽然大多数数学家怀疑机器会很快取代他们职业的创造性方面，但有些人承认技术将在他们的研究中发挥越来越重要的作用 - 这种特殊的壮举可能是其接受的转折点。

Schearze，一个数字化学家，阐述了雄心勃勃的计划 - 他与哥本哈根大学的他的合作垃圾桶共同创作 - 在2019年在德国波恩大学的一系列讲座中，他是基于的。这两位研究人员被称为它“浓缩数学”，他们表示，它有望在远离几何到数字理论之间进行新的洞察和联系。

其他研究人员正在关注：Scholze被认为是数学最耀眼的明星之一，并具有引入革命概念的轨道记录。 Maryland的约翰霍普金斯大学的数学家Manymatician表示，如果Scholze和Clausen的愿景意识到，数学的方式在50年来毕业的方式可能会与今天的不同。 “我认为有很多数学领域将来会受到他的想法的影响，”她说。

到目前为止，大部分愿景都依赖于技术证明，如此，即使是Scholez和Clausen也无法确定它是正确的。但本月早些时候，Scholze宣布了一个通过专门的计算机软件检查证据的核心的项目已经成功。

数学家有长期使用的计算机进行数值计算或操纵复杂公式。在某些情况下，他们通过使计算机做出大量重复性工作 - 最着名的是20世纪70年代最着名的证据，即任何地图都可以用四种不同的颜色着色，而不填写任何两个相邻国家的证据颜色。

但是被称为证明助手的系统更深入。用户将语句输入系统，以教授数学概念的定义 - 基于机器已经知道的更简单的对象。声明也可以是指已知对象，并且证明助手将根据目前的知识来回答事实是否“显然”是真实的还是假。如果答案不明显，则用户必须输入更多详细信息。因此，验证助手迫使用户以严谨的方式阐述他们的论点的逻辑，并且他们填补了人类数学家有意识或无意识地跳过的更简单的步骤。

一旦研究人员就把一组数学概念翻译成校正助手就完成了艰苦的工作，该程序会生成一个可以由其他研究人员构建的计算机代码库，并用于定义更高级别的数学对象。通过这种方式，证明助手可以帮助验证否则耗时和困难的数学证据，也许甚至几乎不可能，对于人类来检查。

帝国伦敦帝国学院的数学家Kevin Buzzard表示，校正助理有长期的粉丝，这是他们第一次在田野的尖端发挥着重要作用，这是一家检查Schoolze和Clausen的合作的一部分结果。 “剩下的剩余问题是：他们可以处理复杂的数学吗？”秃鹰说。 “我们表明他们可以。”

这一切都发生得比任何人想象的要快得多。 Scholze于2020年12月向探索助理专家挑战了他的挑战，并由一群由Johan Commelin领导的志愿者是德国弗赖堡大学的数学家领导的志愿者。 6月5日 - 少于六个月后 - Scholze发布在Buzzard的博客上，实验的主要部分成功了。 “我发现它绝对疯狂，互动证明助理现在处于级别，在一个非常合理的时间跨度，他们可以正式验证困难的原创研究，”Spolze写道。

据Schoolze和Clausen称，浓缩数学的关键点是重新定义拓扑的概念，是现代数学的一个基石。数学家学习的许多物体具有拓扑结构 - 一种确定对象部分靠近哪个结构的结构，而不是。拓扑提供了一种形状的概念，但比熟悉的学校级几何形状更具缺乏态度：在拓扑中，任何没有撕裂物体的转变就可以允许。例如，任何三角形都是拓扑相当于任何其他三角形 - 甚至是圆形 - 但不是直线。

拓扑不仅在几何形状中发挥关键部分，而且在功能分析中，研究功能的研究。函数通常在具有无限数量的空间中“活”（例如是Quantum Mementics的波力事件）。它对称为P-ADIC数字的数字系统也很重要，具有异国情调的“分形”拓扑。

2018年左右，Scholze和Clausen开始意识到拓扑概念的传统方法导致这三种数学宇宙 - 几何，功能分析和P-ADIC数字之间的不兼容性 - 但是该替代基础可以弥合那些差距。许多结果在每个领域的结果似乎在其他领域都有类似物，即使他们显然处理完全不同的概念。但是，一旦拓扑以“正确”方式定义，两位研究人员都会被揭示理论之间的类比是同一“浓缩数学”的情况。克劳森说：“这是一些大统一”的三个领域。

Scholze和Clausen表示，他们已经发现了一些简单的“浓缩”的一些几何事实，并且他们现在可以证明以前未知的定理。他们还没有制作这些公众。

然而，有一个捕获，但是要表明几何形状适合这张照片，Schoolze和Clausen必须对这一套普通实数来证明一个高技术定理，这具有直线的拓扑。 “这就像允许实数进入这个新框架的基础定理一样，”Commelin解释道。

克劳森回忆起Sechze如何无情地在证明之前努力，直到它完成“通过愿意”，在该过程中产生许多原创思想。 “这是我见过的最神奇的数学壮举，”克劳森召回。但争论是如此复杂，Schole自己担心整个企业无效的微妙差距。 “看起来很令人信服，但它只是小说，”克劳森说。

有关帮助检查该工作，Schearze转向Buzzard，这是一个代价理论家，他们是精益的专家，验证助理软件包。精益最初是由华盛顿雷德蒙德的微软研究的计算机科学家创建的，目的是严格检查计算机代码的错误。

Buzzard一直在运行一个多年计划，以编制帝国帝国的整个本科数学课程。他还尝试进入系统进入系统，包括Perfetoid Spaces的概念，这有助于在2018年获得Schole Sender邮票。

Commelin，谁也是一个数字主义者，在努力验证Schearze和Clausen的证据中的努力。 Commelin和Schearze决定将他们的瘦液呼吁液体张量实验，在渐进式摇滚乐队液体张力实验中，其中两种数学家都是粉丝。

随之而来的是发热的在线合作。十几个左右的数学家，倾向于加入的体验，研究人员在路上得到了计算机科学家的帮助。六月初，该团队完全翻译了ScheCze的证据的核心 - 这部分担心他最多 - 倾向于精益。它都检查过 - 软件能够验证证明的这一部分。

Commelin说，Scholze的证据的精益版本包括数万条代码，比原来版本长100倍。 “如果你只是看看精益代码，你将非常艰难地了解证明，特别是现在的方式。”但研究人员称，让证据在计算机上工作的努力帮助他们也能更好地了解。

Riehl是在经过实验助理的数学家之一，甚至在她的一些本科课程中教授它们。她说，虽然她没有在她的研究中系统地使用它们，但他们已经开始改变她认为对构建数学概念和说明和证明他们的定理的做法的方式。 “以前，我想到了截至两种不同的东西，现在我认为它们是一样的。”

许多研究人员表示，数学家不太可能被机器更快替换。校正助手无法读取数学教科书，他们需要从人类的连续输入，他们无法决定数学陈述是否有趣或深刻 - 只有无论是正确的，秃鹰都说。尽管如此，计算机还可以很快指出数学家未能注意到的已知事实的后果。

Schearze说，他对卫生助手的途径有多么惊讶，但他不确定他们是否会在他的研究中继续发挥重要作用。 “现在，我无法真正看到他们如何帮助我作为数学家的创造性工作。”