Cardano创始人承认AI数学进展超出预期

卡达诺创始人查尔斯·霍斯金森：人工智能在数学领域的进展远超预期

卡达诺（Cardano）创始人查尔斯·霍斯金森（Charles Hoskinson）指出，人工智能在数学领域的发展速度远远超出了他的想象。他将近期关于人工智能解决该领域最棘手开放性问题之一的声明视为一个转折点。

未曾预见的进步

在一次YouTube直播节目中，霍斯金森表示，他原本期望形式化系统能协助更大的数学家团队进行协作和验证人类编写的证明。但他并未预料到大语言模型会在如此短的时间内独立生成完整的数学证明。

“我们从未预料到人工智能会深入到这种程度，”霍斯金森说道，并补充称，此前认为人工智能能够完全撰写证明的想法显得“相当遥远”。他指出，人工智能已不仅仅停留在辅助数学家的阶段，目前的系统现在能够独立生成并正式验证复杂的数学证明。

他的评论直接回应了OpenAI的宣布：其内部人工智能系统产生了一个针对纳维-斯托克斯（Navier-Stokes）存在性与光滑性问题的声称解决方案。这一拥有约90年历史、至今未解的难题探讨的是：描述液体和气体运动规律的方程中，三维流体运动是否会在有限时间内发生奇点崩溃。

OpenAI表示，一个“比GPT-6 Astra强大得多的”内部模型生成了一份证明，指出三维纳维-斯托克斯方程可能在有限时间内出现奇点。据《华尔街日报》报道，OpenAI称该系统在约88小时内并行部署了多达1万个人工智能代理，计算成本高达数百万美元。该公司发布了一份165页的证明文件以及一份Lean形式化代码，其中Lean是一种编程语言，用于检查数学论证每一步的逻辑有效性。

对成果来源与研究隐私的质疑

在直播中，霍斯金森称赞这一报告的能力“相当惊人”，同时也指出了关于该工作来源以及提交给基于云的人工智能服务的研究隐私等未决问题。此次宣布并非没有引发争议。

纽约大学数学教授特里斯坦·巴克马斯特（Tristan Buckmaster）发表声明称，他和Anthropic的研究员莱文特·阿尔波格（Levent Alpoge）一直在研究纳维-斯托克斯问题，这项工作始于去年，并使用了包括OpenAI Codex在内的大语言模型混合方案。OpenAI否认访问过私人作品，但无法排除去标识化的使用数据影响模型改进的可能性。

霍斯金森还提出了研究人员与基于云的AI系统分享未发表想法时的担忧。他认为，在使用集中式模型时，学者和企业家可能会暴露其私人研究笔记、知识产权或早期阶段的创意。

目前，克雷数学研究所（Clay Mathematics Institute）仍将纳维-斯托克斯问题归类为“未解决”，等待其发表、同行评审及广泛的数学界认可。

霍斯金森在形式化数学方面有着直接的个人联系。2021年，他向卡内基梅隆大学捐赠了2000万美元，以建立霍斯金森形式化数学中心（Hoskinson Center for Formal Mathematics）。他的言论反映了他对AI辅助数学看法的更广泛转变：从一种主要用于检查和协调人类工作的技术，转变为越来越多地直接参与复杂数学证明构建和验证的系统。