尧图网页设计 
agent 产出的东西谁来验收是我搭工作流最头疼的一环。OpenAI 昨天端出 722 篇模型写的数学论文附一整套验收方案。本周 Top5Agent-Reach6,454、OpenShell5,228、hyperframes3,614、openrig3,327、openGym3,318。本期主角不在上面这张表里它太新了周增统计还没算到它。openai/math 创建于 10 月 6 日深夜到本文写作时不到一天3,615 星、320 forkApache-2.0 协议。仓库里是 722 篇数学手稿出自 OpenAI 一个还没有名字、没有 API、没有定价的内部模型按 372 个结果家族组织横跨 17 个数学分支。其中 162 篇的主结果有 Lean 形式化证明机器能逐行核验剩下 560 篇只有论文本身README 原话说部分未形式化的结果可能有问题。这篇讲三件事这条数学产线怎么跑机器验收到底验了什么数学社区为什么盯得这么紧。图 openai.com 公告页官方横幅它是什么打开仓库先看到的是一批研究档案。preprints/ 目录下每篇论文一个文件夹装着 PDF、LaTeX 源码和引用用的 BibTeX论文落款日期从 9 月 10 日排到 10 月 5 日第二天整包发布。lean/ 目录是一个 Lean 4.34.1 形式化库另附 10 篇推理摘要 PDF节选模型解特定题目时的思考过程合计约两百页。整库 5.8 万个文件。产线流程 README 写得很直白。先给模型出了约 4,000 道开放研究题理由是原有数学评测已经考不出差距平均每道题花约 3 小时 ChatGPT Pro 档位的思考算力产出按显著性筛选后聚成家族一个家族收主结果、伴生论证、推论和另证。4,000 道题出 722 篇论文这个比例别读成解题率筛选标准没有公开OpenAI 自己也承认哪些结果够格是它自己判的。固定流程之外有两个例外zeta 函数零点自由区域的工作和 CM 阿贝尔簇上的 Hodge 猜想证明zeta 那篇 Re(s)11/12 区域的行文还经过人工润色。为什么有意思机器验收只覆盖一小半但验收方式是新的162 篇有 Lean 形式化的论文是这批材料里唯一的硬通货。Lean 是证明助手语言证明写成代码后由内核逐行检查通过与否机器说了算。OpenAI 配的核验工具叫 Comparator配置里只放行 propext、Quot.sound、Classical.choice 三个标准公理证明不许引别的。外部评测 kingy.ai 逐条看过配置后提醒了一个关键区分Lean 核的是形式化陈述形式化陈述跟论文里那句话是不是一回事仍然要人对照。好在这两者都被摊开了每篇论文的 PDF 和对应 Lean 文件并排放着引用条目和版本修订全部留档改过的旧版本不删。跑一遍验证本身是个工程活lean/README 特意提醒整库编译会撞上 Linux 的 vm.max_map_count 上限建议只编小局部要全量编译得用 -DMMAPOFF 重编 Lean再加一组 glibc 环境变量。换句话说想亲手核验这批证明先得过一道系统调优的门槛。这个细节比任何宣传语都诚实形式化验证到今天仍然是有成本的活。治理是这次发布的另一半8 月 1 日 OpenAI 发过一批十大数学进展当时数学圈火气不小有数学家指出模型的关键论证与他 2016 年的论文撞车而发布稿没有标出处科学美国人把研究不端写进了标题。9 月 29 日设在高等研究院的数学与人工智能顾问组发布行为准则要求实验室别拿数学发布当模型营销别在专有模型上刷开放难题发布后要出钱资助人类数学家去理解这些结果。这次 722 篇的发布被普遍读作对那份准则的照做问题数、算力开销、推理摘要、版本制度都按建议给了还承诺出钱办研讨班。两条没做到产生结果的模型没放出仓库还挂在 OpenAI 自己账下而准则希望社区托管OpenAI 说还在找。另外这个仓库的 issue 区是关闭的外人发现证明有问题没有公开入口提交。边界与局限这批材料的可信度分三层看。最硬一层是 162 篇 Lean 主结果机器核过但陈述与论文的对应关系还等着人工抽查。次一层是其余 560 篇纯论文README 明说可能有错。推理摘要只覆盖 10 个家族372 分之 3 都不到想看模型怎么想的基本只能从证明文本反推。头条级结论全部未经同行评审。π 的无理数指数恰为 2、自由群因子全部同构、有理数上的希尔伯特第十问题无解这几个大结论都还没有 Lean 形式化。有个所有狄利克雷 L 函数在 Re(s)7/8 无零点的结果倒是形式化了外部给它起名叫准黎曼猜想但它离真正的黎曼猜想还差半个平面别读成黎曼猜想被证明。想自己跑验证的除了 mmap 那道坎还要有版本意识OpenAI 说在找社区托管方这个仓库地址将来可能变。对谁有价值数学和理论计算机方向的研究者现在就值得深读从 10 篇推理摘要和 162 个 Lean 文件下手那是全部材料里能独立核验的部分。做 AI 基础设施的人可以把这份发布当验收流程的参考设计读问题集、显著性筛选、形式化、版本制度、外部顾问链条齐全直接能抄。写论文想引用结论的人只认有形式化的那 162 篇其余当普通预印本对待。等模型放出再玩的人可以再等等OpenAI 说了会负责任地放没给时间表。我的用法很明确引用只认有 Lean 形式化的那 162 篇其余 560 篇当预读材料。AI 产出怎么验收这个仓库是目前最完整的一份公开答卷。数据截至 2026-10-07来源 GitHub APIopenai/math 元数据、formalization.yaml 逐条计数、lean/README 与 lean-toolchain、openai.com 公告页、外部评测CellCog 2026-10-06、kingy.ai 2026-10-06、theclarity.today 2026-10-06、orcarouter 2026-10-07、Scientific American 2026-08-06GitHub 仓库 https://github.com/openai/math OpenAI 把模型写的 722 篇数学论文搬上 GitHub，只有五分之一过了机器验证
agent 产出的东西谁来验收是我搭工作流最头疼的一环。OpenAI 昨天端出 722 篇模型写的数学论文附一整套验收方案。本周 Top5Agent-Reach6,454、OpenShell5,228、hyperframes3,614、openrig3,327、openGym3,318。本期主角不在上面这张表里它太新了周增统计还没算到它。openai/math 创建于 10 月 6 日深夜到本文写作时不到一天3,615 星、320 forkApache-2.0 协议。仓库里是 722 篇数学手稿出自 OpenAI 一个还没有名字、没有 API、没有定价的内部模型按 372 个结果家族组织横跨 17 个数学分支。其中 162 篇的主结果有 Lean 形式化证明机器能逐行核验剩下 560 篇只有论文本身README 原话说部分未形式化的结果可能有问题。这篇讲三件事这条数学产线怎么跑机器验收到底验了什么数学社区为什么盯得这么紧。图 openai.com 公告页官方横幅它是什么打开仓库先看到的是一批研究档案。preprints/ 目录下每篇论文一个文件夹装着 PDF、LaTeX 源码和引用用的 BibTeX论文落款日期从 9 月 10 日排到 10 月 5 日第二天整包发布。lean/ 目录是一个 Lean 4.34.1 形式化库另附 10 篇推理摘要 PDF节选模型解特定题目时的思考过程合计约两百页。整库 5.8 万个文件。产线流程 README 写得很直白。先给模型出了约 4,000 道开放研究题理由是原有数学评测已经考不出差距平均每道题花约 3 小时 ChatGPT Pro 档位的思考算力产出按显著性筛选后聚成家族一个家族收主结果、伴生论证、推论和另证。4,000 道题出 722 篇论文这个比例别读成解题率筛选标准没有公开OpenAI 自己也承认哪些结果够格是它自己判的。固定流程之外有两个例外zeta 函数零点自由区域的工作和 CM 阿贝尔簇上的 Hodge 猜想证明zeta 那篇 Re(s)11/12 区域的行文还经过人工润色。为什么有意思机器验收只覆盖一小半但验收方式是新的162 篇有 Lean 形式化的论文是这批材料里唯一的硬通货。Lean 是证明助手语言证明写成代码后由内核逐行检查通过与否机器说了算。OpenAI 配的核验工具叫 Comparator配置里只放行 propext、Quot.sound、Classical.choice 三个标准公理证明不许引别的。外部评测 kingy.ai 逐条看过配置后提醒了一个关键区分Lean 核的是形式化陈述形式化陈述跟论文里那句话是不是一回事仍然要人对照。好在这两者都被摊开了每篇论文的 PDF 和对应 Lean 文件并排放着引用条目和版本修订全部留档改过的旧版本不删。跑一遍验证本身是个工程活lean/README 特意提醒整库编译会撞上 Linux 的 vm.max_map_count 上限建议只编小局部要全量编译得用 -DMMAPOFF 重编 Lean再加一组 glibc 环境变量。换句话说想亲手核验这批证明先得过一道系统调优的门槛。这个细节比任何宣传语都诚实形式化验证到今天仍然是有成本的活。治理是这次发布的另一半8 月 1 日 OpenAI 发过一批十大数学进展当时数学圈火气不小有数学家指出模型的关键论证与他 2016 年的论文撞车而发布稿没有标出处科学美国人把研究不端写进了标题。9 月 29 日设在高等研究院的数学与人工智能顾问组发布行为准则要求实验室别拿数学发布当模型营销别在专有模型上刷开放难题发布后要出钱资助人类数学家去理解这些结果。这次 722 篇的发布被普遍读作对那份准则的照做问题数、算力开销、推理摘要、版本制度都按建议给了还承诺出钱办研讨班。两条没做到产生结果的模型没放出仓库还挂在 OpenAI 自己账下而准则希望社区托管OpenAI 说还在找。另外这个仓库的 issue 区是关闭的外人发现证明有问题没有公开入口提交。边界与局限这批材料的可信度分三层看。最硬一层是 162 篇 Lean 主结果机器核过但陈述与论文的对应关系还等着人工抽查。次一层是其余 560 篇纯论文README 明说可能有错。推理摘要只覆盖 10 个家族372 分之 3 都不到想看模型怎么想的基本只能从证明文本反推。头条级结论全部未经同行评审。π 的无理数指数恰为 2、自由群因子全部同构、有理数上的希尔伯特第十问题无解这几个大结论都还没有 Lean 形式化。有个所有狄利克雷 L 函数在 Re(s)7/8 无零点的结果倒是形式化了外部给它起名叫准黎曼猜想但它离真正的黎曼猜想还差半个平面别读成黎曼猜想被证明。想自己跑验证的除了 mmap 那道坎还要有版本意识OpenAI 说在找社区托管方这个仓库地址将来可能变。对谁有价值数学和理论计算机方向的研究者现在就值得深读从 10 篇推理摘要和 162 个 Lean 文件下手那是全部材料里能独立核验的部分。做 AI 基础设施的人可以把这份发布当验收流程的参考设计读问题集、显著性筛选、形式化、版本制度、外部顾问链条齐全直接能抄。写论文想引用结论的人只认有形式化的那 162 篇其余当普通预印本对待。等模型放出再玩的人可以再等等OpenAI 说了会负责任地放没给时间表。我的用法很明确引用只认有 Lean 形式化的那 162 篇其余 560 篇当预读材料。AI 产出怎么验收这个仓库是目前最完整的一份公开答卷。数据截至 2026-10-07来源 GitHub APIopenai/math 元数据、formalization.yaml 逐条计数、lean/README 与 lean-toolchain、openai.com 公告页、外部评测CellCog 2026-10-06、kingy.ai 2026-10-06、theclarity.today 2026-10-06、orcarouter 2026-10-07、Scientific American 2026-08-06GitHub 仓库 https://github.com/openai/math