OpenAI公开前沿模型数学新成果及Lean形式化证明
OpenAI近日公布,其内部前沿模型在数学开放问题上取得了新结果,并已将Lean证明形式化及相关研究细节公开在GitHub上。
Lean是一种交互式定理证明器,能够以形式化语言验证数学证明的正确性。OpenAI此次公开证明形式化,意味着相关推理过程可以通过机器辅助进行严格校验。该公司在官方博客中分享了这些进展,但未透露所解决的具体数学问题。
这一成果展示了前沿模型在数学推理领域的应用潜力,也为研究者提供了可复现的参考材料。OpenAI表示,未来将继续推进AI在数学及其他科学领域的研究。
- 2026-10-09 10:09 | 新浪:陶哲轩质疑OpenAI公司:719篇AI数学证明,人类真的理解了吗?阅读原文
(来源:IT之家) IT之家 10 月 9 日消息,OpenAI 于 10 月公布 719 份 AI 数学解答,涵盖 372 个数学结果族,涉及数百项开放研究问题,不过发布后被指尚未完全达到“数学与人工智能顾问小组”(AGMAI)提出的标准。 IT之家此前报道,OpenAI 于 10 月 6 日最初在 GitHub 发布 722 份 AI 生成数学手稿总数,涉及 372 个结果族及多项开放研究问题。不过于 10 月 7 日因一处符号错误及其连锁影响撤回 3 份,现公开目录为 719 份。 OpenAI 表示,发布前曾咨询普林斯顿高等研究院主持的“数学与人工智能顾问小组”(AGMAI),并...
- 2026-10-09 09:40 | IT之家:陶哲轩质疑 OpenAI 公司:719 篇 AI 数学证明,人类真的理解了吗?阅读原文
IT之家 10 月 9 日消息,OpenAI 于 10 月公布 719 份 AI 数学解答,涵盖 372 个数学结果族,涉及数百项开放研究问题,不过发布后被指尚未完全达到“数学与人工智能顾问小组”(AGMAI)提出的标准。IT之家此前报道,OpenAI 于 10 月 6 日最初在 GitHub 发布 722 份 AI 生成数学手稿总数,涉及 372 个结果族及多项开放研究问题。不过于 10 月 7 日因一处符号错误及其连锁影响撤回 3 份,现公开目录为 719 份。OpenAI 表示,发布前曾咨询普林斯顿高等研究院主持的“数学与人工智能顾问小组”(AGMAI),并参考其公开建议。然而,从公开信...
- 2026-10-08 18:00 | 新浪财经:刚刚,OpenAI撤回了三篇AI数学论文,竟是因为符号写错了阅读原文
编辑|Panda昨天一口气放出 722 篇 AI 数学手稿的 OpenAI,刚刚撤回了其中 3 篇。原因说来简单:一个正负号写错了。刚刚,OpenAI 在 openai/math 仓库中发布了第一份更新日志。日志显示,OpenAI 撤回 3 篇手稿,修订 14 篇,另有 13 篇更新了引用。仓库里的手稿总数从 722 篇降为 719 篇。一个正负号,拖垮三篇论文被撤回的三篇论文,都和千禧年大奖难题之一的霍奇猜想有关:Algebraicity of Weil classes on split abelian eightfoldsAlgebraicity of Kuga–Satake Corres...
- 2026-10-08 16:47 | 36氪:数学难题正被AI批量攻克,数学家却被逼着给AI擦屁股阅读原文
多年以后,面对人工智能,数学家们估计会想起 OpenAI 轰炸数学界的,那个遥远的上午。 10 月 6 号,OpenAI 一口气在 GitHub 上倾泻了 722 份手稿,里面包含了 372 个数学难题的证明研究,给数学家们整了个大的。 这些题有多牛叉咱看不懂,但看数学界内部研究员的反应,可能比上回 GPT 速通千禧年难题还要夸张。 罗格斯大学的数论学家 Alex 直言,这简直是在逗我玩儿,准黎曼猜想都做出来了,菲尔兹奖啥的,给你了呗。 英国皇家学会的研究员 Thomas 更佛系,建议大伙儿休休假,陪陪家人,感受一下自然,然后再回来工作。 没办法,上回的千...
- 2026-10-07 21:08 | Engadget:OpenAI just posted hundreds more results on major math problems阅读原文
The new results are likely to expand AI controversy roiling the mathematics community. New Africa/Shutterstock ...
- 2026-10-07 15:38 | 新浪财经:OpenAI发布700余篇含AI生成解答的数学新论文阅读原文
就在OpenAI宣称攻克数学领域一大难题、在数学界引发激烈争论不到一个月后,这家人工智能公司发布700多篇新研究论文,公布多个数学方向的研究成果。 OpenAI于周二表示,这些全新成果由一款尚未对外发布的模型生成,该模型性能优于市面商用版本。公司在代码托管平台GitHub上发布了722篇论文,内含数百个尚未解决的数学问题的解答。OpenAI称,该做法一定程度上参考了独立机构“数学与人工智能顾问小组”给出的建议。 上月OpenAI公布攻克棘手的“纳维-斯托克斯方程存在性与光滑性问题”之后,便宣布与该顾问小组展开合作。 这次纳维-斯托克斯方程相关成果引发巨大争议:一方面有人质疑Open...
- 2026-10-07 11:56 | 新浪财经:OpenAI一次性公开377项AI数学成果,引发学界验证质疑阅读原文
来源:环球网 【环球网科技综合报道】10月7日消息,据gizmodo报道,OpenAI发布一批由内部未发布前沿模型生成的数学研究成果,共含377项数学成果,涉及数百个长期悬而未决的数学开放问题。据悉,此次发布的手稿涵盖数论、代数几何、理论计算机科学、统计力学等多个数学分支。而此次发布正值数学界对AI生成数学成果的传播方式持续争论之际。2026年9月下旬,由普林斯顿高等研究院托管的数学与人工智能咨询小组(AGMAI)成立,该小组在9月底发布首批建议,呼吁AI实验室通过成熟学术渠道发布成果,披露模型名称、提示词和算力成本等关键信息,并明确提出不应将数学成果发布用作模型营销工具。OpenAI在发布说...
- 2026-10-07 11:12 | 中国科技网:OpenAI发布722篇数学手稿,包含数百个“未解问题答案”阅读原文
2026-10-07 11:12:12 来源: 科技日报 点击数: 0 ...
- 2026-10-07 10:24 | 华尔街见闻:数学大爆炸!OpenAI 一夜攻克722个数学难题,准黎曼猜想已被证明阅读原文
OpenAI又要惹众怒了! 就在今天,全球数学界和AI界都被这个消息震惊了—— 没有预警,没有经过同行评审,甚至无视了学术界长久以来的礼仪,OpenAI发布了一系列由内部前沿模型产生的新数学成果。 他们简单粗暴地接放出GitHub项目库 math 。 里面是722 篇数学手稿,涵盖了 372 个此前悬而未决的顶级数学难题家族。 其中,OpenAI 未发布的 AI 模型证明了拟黎曼猜想,并同步发布了 Lean 形式化验证。如果经过证实,这将是数论领域的历史性突破,也是 AI 发展史上的里程碑时刻! 根据 OpenAI 的披露,绝大多数难题的证明,仅仅花费了他们未发布的一个内部模型平均 3 小时...
- 2026-10-07 09:50 | gizmodo.com:OpenAI Dumps 377 New Math Results on GitHub, Publishes Hand-Wringing Blog Post阅读原文
On Tuesday, OpenAI continued its all-out assault on mathematicians’ peace of mind and sense of career stability by releasing 377 new math results in the form of an info-dump on GitHub. What kinds of accomplishments is OpenAI claiming now? Well, one paper chosen at random claims to have proven “the f...
- 2026-10-07 08:00 | 新浪财经:OpenAI发布又一批AI数学研究成果,攻破数百个悬而未决难题阅读原文
炒股就看金麒麟分析师研报,权威,专业,及时,全面,助您挖掘潜力主题机会! (来源:IT之家)IT之家 10 月 7 日消息,OpenAI 在一批包含 722 份手稿、涵盖 372 个结果家族的文件中,公布了某款未发布的前沿模型解决的多项长期存在的数学难题。IT之家注意到,这一举措延续了其一系列突破性成果,这些成果既给数学界部分人士留下了深刻印象,也引发了不安,同时还带来了关于研究伦理和学术行为的疑问。据负责以负责任的方式传达这些成果、新成立的精英数学家独立咨询小组 AGMAI 介绍,此次公布的内容包含对“数百个”未解决问题的解答。数周以来外界一直在期待这批成果,不过在此之前,OpenAI 始...
- 2026-10-06 20:00 | OpenAI:Sharing AI progress in mathematics阅读原文
OpenAI publishes new results on open problems in mathematics from an internal frontier model and shares Lean proof formalizations and research details on GitHub.
- 2026-10-06 19:05 | 36氪:数学大爆炸,OpenAI 一夜攻克722个数学难题,准黎曼猜想已被证明阅读原文
就在今天,全球数学界和AI界都被这个消息震惊了—— 没有预警,没有经过同行评审,甚至无视了学术界长久以来的礼仪,OpenAI发布了一系列由内部前沿模型产生的新数学成果。 他们简单粗暴地接放出GitHub项目库math 。 链接:https://github.com/openai/math/ 里面是722 篇数学手稿,涵盖了 372 个此前悬而未决的顶级数学难题家族。 链接:https://github.com/openai/math/blob/main/overview.pdf 其中,OpenAI 未发布的 AI 模型证明了拟黎曼猜想,并同步发布了 L...