OpenAI最近在GitHub上放了份实打实的东西：内部前沿AI模型攻克了一道数学公开难题，还把Lean语言写的形式化证明和完整研究细节全开源了。
到底分享了什么？
就是两部分——一是内部那台还没完全对外披露细节的前沿AI模型，解决了数学领域公认的公开难题；二是把这个难题的证明过程，转换成了Lean的形式化代码，所有研究的步骤、调整的细节，都原原本本贴在GitHub上了。Lean是数学圈里常用的形式化验证工具，能把数学家的自然语言推导，变成机器能逐条、无歧义验证的代码。这次OpenAI放的，就是把AI怎么解这个题的“解题思路草稿”，变成了机器能查的“标准答案”。
这事的核心门道在哪？
之前AI在数学上的突破，大多是“只报结果”——比如“我们的AI解了个题”，但背后的推导是黑箱，没法验证对错，也没法复用。这次的关键，是把“不可验证的AI成果”变成了“可公开核对的研究资产”。你要是懂Lean，就能去GitHub上逐行看AI的证明步骤，哪一步对，哪一步有调整，甚至能改改参数测不同的解法。对数学研究者来说，这省了从头研究的功夫——不用自己再推导一遍AI已经证过的内容，直接拿过来改改思路就行。
对圈子来说意味着什么？
这事对AI圈子来说，相当于开了个新玩法。以前大公司在前沿研究上要么藏着核心模型细节，要么只吹成果，OpenAI这次选择把“解题的过程”全公开，相当于给AI数学研究定了个新的透明度标杆。其他做AI+数学的团队，接下来要么得跟上这种公开的节奏，要么得找出更有说服力的证明方式。对数学学界来说，这也是新鲜事——第一次有AI能解公开难题，还把证明摆到台面上给人查，不是靠一张嘴说“我对了”。
现在不少AI公司在基础研究上要么捂得严严实实，要么只放些模糊的成果，OpenAI这次的做法会不会变成行业默认的公开新规则？
素材来源：OpenAI News · AI情报、AI应用落地、开源生态、科研前沿
查看报道原文
发表第一条评论吧