OpenAI 开源数学论文与证明成果仓库，含 722 篇手稿与 Lean 形式化

OpenAI 在 GitHub 开源了一份数学论文与证明仓库，包含 722 篇由内部模型生成的数学手稿，归为 372 个研究族类，多数配有 Lean 形式化证明。模型被投喂约 4,000 个开放问题，平均每项结果使用 3 小时 ChatGPT Pro 思考算力，部分成果涉及黎曼 ζ 函数无零点区域与 Hodge 猜想证明。