AI助攻「菜鸟数学家」解决忙碌海狸问题，陶哲轩转发分享
在 AI 的帮助下，越来越多的数学问题得到了解决。
AI在数学领域的应用对大家来说并不陌生了。
数学家陶哲轩作为倡导者，一直走在使用AI辅助证明的前沿。他倡导使用像Lean和Coq这样的证明助手工具。这些工具可以形式化和验证复杂的数学证明，减少人为错误的可能性。也有不少数学家在他的启发下有了新成果，例如利用AI形式化费马大定理的证明。他参与了由Talia Ringer发起的AI在数学中资源列表的推广和编辑工作。这个资源列表专注于 AI for Math，为那些希望进入数学 AI 领域的人提供帮助。
陶哲轩在推进项目研究进展的同时，还试着学习如何创建动画图表，他决定对零密度估计进行文献回顾 。他讲到，自己一直很好奇为什么没有一份全面的综述来涵盖这些年来建立的所有零密度定理，现在他清楚了，是因为文献太过复杂，尤其在3/4≤σ＜1的这个范围， 使用了多种方法。界限通常是逐段的，主要是因为这些方法依赖于控制整数矩而不是分数矩。然而，这些界限虽然以人类可读形式陈述时显得杂乱，但对计算机来说却很容易处理。
陶哲轩将所有的界限汇总到一个Python文件中，并用它创建了附带的动画。
在这一博客的评论中，陶哲轩补充道：
“不得不说，我确实使用了一些AI辅助来帮助编写代码。在某种程度上，我将AI辅助视为一种心理支持——当我知道除了传统的调试和搜索方法外，还有AI工具可以提供初始代码并自动完成部分代码时，更容易说服自己花时间编程。不过，我发现这些工具在调试方面并不是特别有用。不过，GPT能够快速创建一个简单的动画测试函数，并且在第一次尝试时就成功编译了。尽管如此，我仍花了大部分时间来调整和调试，才得到了我想要的动画。”
显然，这次尝试的结果还不错。后续陶哲轩还转发了一篇文章，生动地展示了数学智能助手如何帮助一群「菜鸟数学家」解决了数学界最难解的问题。
程序员通常希望最大程度减少代码运行所需要的时间，忙碌海狸函数（BB(n））这个计算机科学中的经典问题却在探寻，一个简单的计算机程序在终止之前可以运行多长时间，即图灵机在特定状态和符号数量限制下所能达到的最大运行步数。
最近的研究表明，寻找长时间运行的计算机程序可以揭示数学知识的现状，甚至告诉我们哪些是可知的。忙碌海狸游戏为评估某些问题的难度提供了一个具体的基准，例如未解决的哥德巴赫猜想和黎曼假设。它甚至提供了一个探索数学逻辑计算极限的视角。
那要怎么理解忙碌海狸函数呢？想象一个小机器人(图灵机)，它有一套指令(对应图灵机的状态)，可以在一条无限长的纸带上移动和写字。纸带最开始是空白的。这个机器人的目标是尽可能多地在纸带上写字，然后停下来。忙碌海狸问题就是要找到这样的机器人，在给定状态数量下可以写最多字的情况。
单规则的情况很简单，因为实际上只有两种可能性。如果规则规定图灵机在看到 0 时停止计算，它将在第一步停止。有了两条规则，就有超过 6,000 个不同的图灵机需要考虑；有了三条规则，这个数字就会膨胀到数百万，有了四条规则，这个数字就会膨胀到数十亿。手工计算所有这些情况是不可能的。
这意味着这个问题只能借助计算机来解决。一个简单的程序可以算出 BB(2) = 6。但 BB(3) 已经很难找到了。而更棘手的是无限循环问题。有的时候图灵机并没有真正停机，而是陷入了无限循环。研究人员需要找到一种判断图灵机是否真正停机的判断方法。
拉多推出忙碌海狸挑战后不久，一些研究人员就开始了搜寻。从1964年到1974年， Allen Brady花了十年，证出了BB(4) 的数值。研究启动时，他还是俄勒冈州立大学数学系研究生，发表时，他已然成为内华达大学雷诺分校的计算机科学教授。
…
参考链接：
https://mathstodon.xyz/@TaliaRinger/112719444060361451
https://mathstodon.xyz/@tao
https://www.quantamagazine.org/how-the-slowest-computer-programs-illuminate-maths-fundamental-limits-20201210/
感谢阅读！如果您对AI的更多资讯感兴趣，可以查看更多AI文章：GPTNB。
AI助攻「菜鸟数学家」解决忙碌海狸问题，陶哲轩转发分享
