AI独立解决30年数学问题变体，陶哲轩分享自动化研究经验

机器之心 报告 机器之心 新闻中心 鄂尔多斯124号的弱化版本最近被展示。自从 1984 年《算术杂志》上一篇题为“整数幂集的完整序列”的论文提出以来，这个问题近 30 年来一直没有得到解决。 Boris Alexeev 博士证明了这个问题。普林斯顿大学数学博士。他使用 Harmonic 的数学人工智能代理亚里士多德来解决这个问题。该代理最近进行了更新，具有更强大的推理功能和自然语言界面。一些有关该主题的报道声称人工智能已经完全自行解决了这个问题，但事实并非如此，并引起了很多争议。鲍里斯·阿列克谢耶夫安排了这件事。在形式猜想项目中，推论涉及形式陈述。不幸的是，这个声明中有一个错字；在显示公式中，注释显示为“≥1”，但在相应的精益语句中，它显示为“=1”。 （这削弱了该主张。）因此，我们还解决了该问题并包含了修改后的主张的证据。最后，我从声明中删除了我认为不必要的部分。亚里士多德证明了这一点。正如 DesmondWeisenberg 提到的，1 的幂（这里等于个位数）存在问题，这意味着 [BEGL96] 中的预测与此不同。我认为 [Er97] 中的版本与此处的描述相符。原因之一是 [BEGL96] 显然缺乏所需的最大公约数条件。目前，无法获取[Er97e]并验证其包含的语句。考虑到亚里士多德的成就，这个话题如此敏感真是可惜。然而，Mathematical Agent 独立证明了鄂尔多斯问题 #124 的简单版本，而且 stillía 具有令人惊讶的数学证明能力。我展示了它。鄂尔多斯第124号的内容如下： 这仍然是一个悬而未决的问题，因为证明中存在一个微妙的错误。鄂尔多斯问题#124 链接：https://www.erdosproblems.com/forum/thread/124 Math AI Agent Aristotle 是一个用于自动形式化和形式验证的 API。 Harmonic 表示，它有能力使用 IMO 黄金级引擎解决最复杂的推理问题。自动将英语陈述和测试转换为经过验证的 Lean4 测试。自动利用整个定理和定义、依赖关系和 Mathlib 库，无缝集成到您的项目中。亚里士多德链接：https://aristotle.harmonic.fun/（鄂尔多斯第124期）在讨论中，Tsav简单介绍了亚里士多德对这个问题的证明方法，称其“简单得惊人”。详细的测试过程，我阅读了，有兴趣的可以查看：https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md Terence Tao非常注重对完整数学问题的独立AI测试。您的评论也在这个问题下方。陶哲轩对数学AI工具的看法保持一致。他认为，与现实世界中的许多其他分布一样，数学中的开放问题表现出典型的“长尾”结构。在数学未解决的问题中，有许多问题比较简单，没有受到太多关注。利用人工智能强大的自动化和推理能力来大规模克服这些问题将带来许多唾手可得的成果。陶哲轩去年在领导方程理论项目时亲眼目睹了这一点。这个项目攻击了代数通用中2200万的含义。使用简单的自动化方法进行的初始扫描在几天内解决了大部分问题，随后采用越来越复杂的方法删除了顽固地抵制先前扫描的剩余实例。我慢慢地破解了它。最新的影响需要人类数月的努力才能最终解决。在这个项目中，陶哲轩获得了大规模自动化数学方面的宝贵经验。加州研究。他以个人日记的形式完整记录了自己研究的详细过程、方法、结果和个人想法。日志链接：https://github.com/teorth/equational_theories/wiki/Terence-Tao’s-personal-logErdos Problem网站是一个类似的例子。该网站目前至少包含 Erdos 的一篇文章中提出的 1,108 个问题。是的，它包含了一些非常困难的经典问题，但还有许多更特殊的问题，甚至连鄂尔多斯本人也没有太多关注。与他在方程论方面的经验类似，陶哲轩现在开始专注于使用自动化技术消除潜在的“容易实现的目标”。几周前，网站上仍标记为开放的一些问题突然被归类为“已解决”。人工智能驱动的文献搜索工具发现这些答案实际上存在于文献中。研究这些问题的数学家正在将人工智能工具与形式证明相结合渴望使用精益来验证现有的证明，生成与这些问题相关的整数序列项，并完成某些解决方案中缺少的推理步骤。陶哲轩认为，鄂尔多斯问题#124的证明属于另一种“唾手可得的果实”，由于描述中的技术遗漏而变得出乎意料的简单。解决问题很容易。具体来说，鄂尔多斯的问题#124在三篇论文中提出，其中两篇论文省略了重要的假设，导致该问题成为基于这两个公式对已知结果（布朗准则）的直接推论。然而，直到鲍里斯·阿列克谢耶夫（Boris Alexeev）使用亚里士多德的工具来解决这个问题时才发现这一点。亚里士多德自主地找到了这个弱化版本的解决方案，在几个小时内（精益）已经正式化。研究人员现在正在系统地检查网站上剩余的问题，寻找更多类似的错误或简单的解决方案。短期来看，这些努力仍然是首要任务rily 专注于“长尾”的末端。但这表明自动化工具在帮助人类数学家在另一个层面上解决这些问题方面正在不断改进。也就是说，消除较容易的部分，以便更清楚地看到真正困难的问题。我们可能已经处于数学重大转变的边缘，因为人工智能可以自己解决数学问题。数学Vibe测试时代已经悄然到来。
特别提示：以上内容（包括图片、视频，如有）由自有媒体平台“网易账号”用户上传发布。本平台仅提供信息存储服务。
注：以上内容（包括图片和视频，如有）由网易号用户上传发布，网易号是一个仅提供信息存储服务的社交媒体平台。