OpenAI在GitHub公开了由未发布前沿大模型生成的722篇数学论文手稿,涵盖17个学科,并包含部分Lean形式化证明。数学界预计需数月验证这些证明是否包含真正的新思想。
OpenAI 在 GitHub 公开了一个包含 722 篇数学论文手稿的仓库,这些手稿被归类为 372 个「结果家族」。据《科学美国人》报道,OpenAI 称这些论文由一个未公开的内部前沿大模型生成。数学界预计需要数月时间才能完成审查,以判断这些证明究竟蕴含着真正的新数学思想,还是仅仅重组了已知结论。
一个月前,OpenAI 曾宣布同一套内部系统证明了三维纳维-斯托克斯方程(Navier-Stokes)可在有限时间内产生奇点。该问题为克雷数学研究所设立的千禧年大奖难题之一。此前这一声明已因署名归属、透明度以及发布节奏等问题引发持续争议。
这批成果横跨 17 个学科,其中理论计算机科学、组合数学、代数几何和数论占比最高。公开目录中声称解决的难题包括:π的无理性指数、马勒猜想(Mahler conjectures)、NP 困难性、自由群因子的同构问题以及相对论性弗拉索夫-麦克斯韦方程组(Vlasov-Maxwell)。
OpenAI 还同步发布了许多证明的 Lean 形式化代码。Lean 是一种允许计算机逐步验证证明逻辑的编程语言。不过,并非所有手稿都已完成形式化。该仓库的说明文件警告称,部分未形式化的结果「可能存在缺陷」,形式化清单也将其审核状态标注为「未核验」(unchecked)。
OpenAI 表示,该模型在评估过程中共尝试了约 4000 个数学问题。平均每个结果消耗的算力约相当于「ChatGPT Pro 思考 3 小时」。仓库中附带了 10 份关于模型推理过程的节选摘要,但 OpenAI 未披露总资金成本、Token 消耗量或公开的模型标识。
OpenAI 称,此次发布参考了新泽西州普林斯顿高等研究院下设的数学与人工智能独立顾问组的建议。该顾问组曾建议 AI 实验室公开模型名称、所用提示词以及每项成果的算力成本,并将成果存入不受任何 AI 实验室控制的中立仓库中。
然而,OpenAI 并未公开提示词与单项算力数据。公司发言人表示,OpenAI 重视这些准则但不受其约束。该发言人同时透露,几乎所有结果都来自向单个 AI 智能体输入的单条提示词,不过部分问题可能经历了多次尝试。
针对这一发布,学术界观点分歧明显。麻省理工学院(MIT)数学家 Andrew Sutherland 表示:「我们应该索要凭据。」他认为在模型正式发布之前,所谓『一次性解决问题』的主张都应视为未经验证。多伦多大学的 Daniel Litt 则持乐观态度:「在我看来,这对数学来说将是一件好事。」
OpenAI 表示,计划资助研讨会和学术会议,帮助数学家理解 AI 生成的研究成果,并正在推进「负责任地发布背后模型」的相关工作。
免费获取企业 AI 成熟度诊断报告,发现转型机会
关注公众号

扫码关注,获取最新 AI 资讯
3 步完成企业诊断,获取专属转型建议
已有 200+ 企业完成诊断