OpenAI公开前沿大模型数学研究成果，含可机验的Lean形式化证明

OpenAI通过GitHub代码库公开其内部前沿大模型生成的一系列全新数学研究成果，其中包含Lean语言形式化证明，数学证明可直接由计算机完成校验。发布同时附带论文修订与引用的规范协议，单份成果平均消耗的算力约等于ChatGPT Pro三小时的深度推理时长。