AI工具独立证明Erdős问题变体,陶哲轩力挺自动化研究
12月01日,据机器之心报道,普林斯顿大学数学博士Boris Alexeev借助数学AI智能体Aristotle(由Harmonic开发),在数小时内独立证明了Erdős问题#124的弱化版本。该问题由著名数学家Paul Erdős提出,自1984年发表在《算术杂志》上以来一直悬而未决,核心涉及整数幂集的完备序列。
此次突破的关键在于:原始问题在三篇早期论文中存在表述差异,其中两篇遗漏了关键假设,导致所形成的弱化版本意外地可通过已知的Brown判别法直接解决。Aristotle通过自然语言界面理解问题描述,并自动生成可在Lean4中验证的形式化证明,展现了高效的自动化推理能力。
著名数学家陶哲轩(Terence Tao)对此表示关注,并在讨论中分享自动化研究经验。作为2006年菲尔兹奖得主、UCLA讲席教授,陶哲轩是当代最活跃且最具影响力的数学家之一——他不仅曾解决困扰学界80余年的Erdős差异问题,近年来更积极推动AI与形式化证明在数学研究中的应用。他认为,数学未解决问题呈“长尾”分布,AI能帮助规模化攻克相对容易的问题,摘取“低垂的果实”。
陶哲轩去年运行Equational Theories项目时,使用自动化方法在几天内解决了2200万个蕴含式中的相当大部分。他建议研究者系统性地扫描剩余问题,寻找更多快速解决方法。
目前Erdős问题网站收录1108个问题,研究者正结合AI工具和形式化证明助手,集中清理底层问题。Aristotle智能体已在GitHub开源证明过程。