OpenAI发布数学手稿库，719份结果中约42%已Lean形式化
OpenAI开源内部模型生成的719份数学手稿，其中约42%的核心结果附带Lean 4机器可验证证明。
重要性实质性证据E3 可检验写法快讯
OpenAI于10月6日在GitHub发布openai/math仓库，公开由内部未发布模型生成的719份数学手稿。
这些手稿归入372个结果家族，覆盖数论、几何等17个领域。每个家族包含主结果及伴随论证或替代证明。
仓库README显示，约42%的顶级结果已完成Lean 4形式化，具备机器可验证性。其余未形式化结果可能存在错误，官方称将尽快修复并持续更新。
该归档采用Apache-2.0许可，旨在提供AI生成数学结论的可复现证据，但并非所有结果均经同行评审或完全验证。