OpenAI在GitHub公开了372项由AI生成的数学成果，其中包含用于机器验证的Lean形式化内容。每项成果平均消耗约3小时的ChatGPT Pro计算资源。这次公开的重点是数学结果及其验证材料，而非新模型或新产品。
Lean形式化是把数学命题和证明写成计算机能够检查的形式，让验证不只依靠读者审阅自然语言推导。此次材料将AI生成数学成果与机器检查结合，为学术界检验这些结果提供了具体对象。
数学界的争论则集中在成果数量与研究价值之间。25位菲尔兹奖得主警告，大规模生产数学真命题可能破坏孕育新思想的研究土壤，而不是催生新的思想。他们质疑的重点，是批量产出能否真正推动数学研究，而非单纯增加可验证结果的数量。
这些成果公开后，研究者可以围绕具体命题、证明及形式化材料展开检验。AI能够生成多少结果，以及这些结果能否形成有价值的数学发现，成为此次公开引出的直接讨论。据The Decoder报道。
来源：The Decoder