OpenAI在GitHub上发布372个AI生成的数学证明
decoder ·
OpenAI在GitHub上发布了由内部AI模型生成的372个数学成果,旨在解决或推进与黎曼猜想等相关的开放性问题。这些证明主要通过单一提示词和智能体生成,每项结果消耗约三小时的ChatGPT Pro算力。为应对可能压垮人工审查流程的海量输出,许多证明附带了Lean形式的形式化验证,以便机器检查。公司选择GitHub而非传统同行评审期刊,表明常规学术出版速度已跟不上这一发现节奏。尽管OpenAI咨询了包括菲尔兹奖得主在内的顾问小组,但数学家们并未对成果的产出速度和数量拥有话语权。数学界反应不一,从兴奋到因大规模生产证明带来的影响而感到沮丧。包括25位菲尔兹奖得主在内的批评者警告称,过度关注解题输出可能会削弱概念理解和真正的洞察力。因此,人们担心AI生成文献的快速扩张最终将超出人类的理解能力。
decoder