OpenAI 公开前沿模型求解数学开放问题的结果与 Lean 证明
OpenAI 让内部前沿模型去做数学开放问题，并把 Lean 形式化证明和研究细节放到 GitHub，供外部复核。
OpenAI 公布了一批由内部前沿模型（frontier model，指能力最强、尚未对外发布的模型）在数学开放问题上取得的新结果，并把对应的 Lean 证明形式化（Lean 是交互式定理证明器，能逐步验证证明是否成立）以及研究细节一并发布到 GitHub。
正文摘录
OpenAI 发布了一个内部前沿模型在数学未解问题上取得的新结果，并在 GitHub 上公开了 Lean 证明形式化（Lean 是一种交互式定理证明器）与研究细节。