OpenAI 公布内部前沿模型在数学开放问题上的新进展并开源 Lean 证明形式化

OpenAI 发布内部前沿模型在数学开放问题上的最新结果，并在 GitHub 上分享 Lean 证明形式化与研究细节。具体题目、模型名称及性能指标原文未给出。可供研究者参考其形式化证明与相关代码以推进数学问题的自动化求解。