币圈界报道:

AI独立生成数学证明引发学界震动

卡达诺项目发起人查尔斯·霍斯金森指出,当前人工智能在数学领域的演进速度远超其最初设想,尤其在处理高难度开放性问题上展现出前所未有的能力。

智能体自主完成复杂证明挑战

在一次公开直播中,霍斯金森坦言,他曾预期形式化工具仅能辅助大型数学团队协作验证人工撰写的推导过程,却未料到大语言模型能在极短时间内独立构建完整且逻辑严密的数学论证。

“我们从未想过它会走到这一步,”他强调,此前认为机器可完全撰写严谨证明的想法仍属遥远幻想。如今,系统不仅具备生成能力,更可实现自我验证,标志着技术角色的根本性转变。

OpenAI公布纳维-斯托克斯问题新解

该观点直接回应了OpenAI近期披露的一项声明:其内部研发的超大规模模型在约88小时内协调1万个代理并行运行,耗资数百万美元,产出一份关于纳维-斯托克斯方程存在性与光滑性问题的主张解决方案。

该问题自上世纪初以来悬而未决,核心在于三维流体运动是否可能在有限时间内出现奇点崩溃。报告包含165页文本及基于Lean语言编写的可形式化代码,用于逐行校验推理链条的逻辑一致性。

学术伦理与数据安全存隐忧

尽管认可成果的技术震撼力,霍斯金森也对研究透明度与隐私保护提出质疑。他指出,当前集中式云平台的使用模式可能使科研人员面临研究成果泄露风险。

纽约大学教授特里斯坦·巴克马斯特及其合作者莱文特·阿尔波格曾开展类似研究,虽未被证实遭数据窃取,但无法排除匿名化训练数据对模型性能的间接影响。霍斯金森提醒,学者在向云端系统提交未发表构想时,需警惕知识产权外泄与创意提前暴露的风险。

目前,克雷数学研究所尚未将此成果列为已解决,仍要求经过正式发表、同行评审与广泛验证程序。

霍斯金森本人长期推动形式化数学发展,2021年向卡内基梅隆大学捐赠2000万美元设立霍斯金森形式化数学中心。他的立场变迁反映出人工智能正从辅助验证工具,逐步演变为深度参与数学发现与建构的核心力量。