小乐数学科普：计算机科学家如何重新构想数学证明——《量子杂志》每周数学随笔

文摘 2025-01-10 08:34 加拿大

每周量子杂志都会解释推动现代研究的最重要理念之一。本周，计算机科学特约撰稿人Ben Brubaker解释了计算机科学的发展如何改变了数学中最古老的概念之一。

图源：Nash Weerasekera | Quanta

作者：Ben Brubaker（量子杂志撰稿人）2025-1-6

译者：zzllrr小乐（数学科普公众号）2025-1-7

原则上，数学家只要坐在舒适的扶手椅上，认真思考，然后一步一步地写出论点，就可以发现新的真理。这种设计证明的基本方法可以追溯到2000多年前（尽管扶手椅是最近添加的）。但证明不仅适用于数学家，在过去的几十年里，理论计算机科学家已经开发出全新的方法来思考它们。

对于计算机科学家来说，证明的关键特性是很容易检查结果是否有效。例如，我们经常让计算机解决难以手动解决的问题。在这些情况下，最好有某种严格的保证——即一个证明——计算机的解确实是正确的。对于计算机科学家关心的许多问题来说，这是可能的，但不是全部。

在1980年代，少数计算机科学家开始想知道，如果计算机的正确性证明不必像普通数学证明那样写下来，情况会如何变化。也许交互式过程可以帮助他们验证更多问题的解？这是一个吸引人的想法，植根于真正的数学家们互相说服他们的论点是有效的方式。

“你正在与你的学生互动，他们可以问你不同的问题，”去年秋天我与计算机科学家汤姆·古尔（Tom Gur）交谈时说。“也许这其中有更大的力量。”

事实上，研究人员很快发现交互式证明比普通证明强大得多——它们可以验证更难的问题的解。但交互式证明只是一个开始。从那以后的几十年里，计算机科学家一次又一次地重新发明了证明。他们的发明对数学和计算机科学的其他分支，甚至量子物理学都产生了深远的影响。

最新值得注意的内容

新型证明往往违背了我们对令人信服的论点应该如何运作的直觉。对于普通的数学证明，只有了解论证细节的读者才能确定它是有效的。读者还必须消化整个证明：一个不耐烦的读者如果跳过一些步骤，可能会错过论点中的缺陷。事实证明，这些性质实际上都不是必需的。在1980年代，计算机科学家发明了“零知识证明” https://www.quantamagazine.org/how-to-prove-you-know-a-secret-without-giving-it-away-20221011/ ——一种在不透露任何关于为什么是真的信息的情况下证明一个陈述是真的的方法。十年后，他们发明了“概率可检验证明”（PCP，probabilistically checkable proof）小乐数学科普：计算机科学家如何学会重新发明证明——译自Quanta Magazine量子杂志，另请参阅小乐数学科普：PCP定理简史——概率可检验证明，它可以说服只阅读一小段论证的人。去年，三位计算机科学家 https://www.quantamagazine.org/computer-scientists-combine-two-beautiful-proof-methods-20241004/ 终于想出了如何将这两种证明技术的理想版本结合起来。在我写了一篇关于这一突破的文章一个月后，该团队进一步推动了他们的结果。https://arxiv.org/abs/2411.07972

在计算机科学家发现交互式证明的强大功能后，他们很快就转向了更复杂的证明程序，涉及两个以上参与者之间的交互。事实证明，这些“多证明者交互证明” 仍然可以验证更难的问题的解。但是，当研究人员将研究扩展到涉及多台量子计算机的交互式证明时，他们的发现并没有做好准备。Kevin Hartnett报告了他们在2020年令人震惊的发现 https://www.quantamagazine.org/landmark-computer-science-proof-cascades-through-physics-and-math-20200304/ ，即这些证明可以验证任何可以想象的计算结果。事实证明，这一发现对数学和物理学中看似无关的问题 https://www.quantamagazine.org/mathematicians-grapple-with-sudden-answer-to-connes-embedding-conjecture-20200408/ 产生了影响。

计算机科学和数学证明之间的另一个联系对数学研究的实践产生了更直接的影响。它被称为Curry-Howard对应关系，是证明和计算机程序之间的精确等价物。Sheon Han在量子杂志一篇解释文章中分解了它的工作原理小乐数学科普：数学证明和计算机程序等同的深层链接——译自Quanta Magazine 。此链接是“证明助手”程序 https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ 的基础，这些程序帮助数学家验证其证明的正确性。正如我的同事Jordana Cepelewicz在2024年3月25日所写的那样 https://mailchi.mp/simonsfoundation/why-classical-computers-can-still-win-quantum-contests-2492262 ，证明助手为数学家开辟了新的合作方式。他们还使没有传统学术背景的研究人员更容易进入该领域——我去年最喜欢的故事 https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/ 记录了一个特别鼓舞人心的例子。

网络上的报道

Wired杂志的YouTube频道提供了一系列精彩的视频，研究人员在其中以五个不同的复杂程度解释了一个概念。我真的很喜欢计算机科学家Amit Sahai用隐藏在企鹅群中的海鹦的照片向一个10岁的孩子解释零知识证明 https://www.youtube.com/watch?v=fOGdb1CTu5c 的方式。

计算机科学家托马斯·维迪克（Thomas Vidick）是2020年关于量子纠缠如何影响交互式证明的论文的合著者，他写了一篇长篇博文 https://mycqstate.wordpress.com/2020/01/14/a-masters-project/ ，记录了他14年来获得这一里程碑式结果的旅程，该结果建立在十几名研究人员的见解之上。

在YouTube频道Computerphile的视频中，计算机科学家Thorsten Altenkirch对证明助手的工作原理以及它们如何帮你避免逻辑谬误进行了有趣的概述 https://www.youtube.com/watch?v=prYaTrZUces 。