形式化证明

分享数学领域的 AI 进展

OpenAI 公布了一批数学开放问题的新结果，这些问题是由其内部的前沿模型解决的。所谓“开放问题”，就是数学界长期没有找到答案的难题；“前沿模型”指能力最强、尚未对外公开的模型。为了让结果可验证，OpenAI 把用 Lean 写出的证明形式化代码以及研究细节放到了 GitHub 上，Lean 是一种能逐步检查数学证明是否成立的工具。对读者来说，这些结果和代码可供查看和复核，说明 AI 在数学证明上又向前走了一步。