OpenAI 以 Lean 证明、推理摘要和计算统计披露 AI 数学成果

在既有数学评估趋于饱和后，OpenAI 使用未公开的内部模型研究开放数学问题，并把本次成果及支持材料放入公开仓库。披露过程参考独立数学与AI咨询组的建议，提供论文修订和引用规则，部分证明附带可由计算机检查的 Lean 形式化材料；尚未形式化的结果可能存在问题，项目承诺持续修订。为解释成果怎样得到，发布方还提供10份模型推理摘要、所尝试问题的统计及以 ChatGPT Pro 思考等价计算量表达的投入。官方称平均每项结果约相当于三小时Pro思考计算，这不是用户实际账单或墙钟耗时。本实践的可借鉴之处是成果验证和披露流程，而不是内部模型已经公开可用，也不能把材料数量当作全部验证成功的定理数。