Lean形式化证明相关资讯

OpenAI公开722篇AI数学手稿：最大规模公开基准背后的透明度博弈

2026年10月6日，OpenAI将一款未发布内部模型产出的722篇数学手稿推上GitHub，覆盖372个问题族，附Lean形式化证明，平均每项结果消耗约三小时ChatGPT Pro算力。普林斯顿高等研究院数学与AI咨询组AGMAI参与制定