AI 如何做出数学发现【导读】-OpenAI 的这 62 页究竟是什么？从“发现笔记”到可验证数学

OpenAI 公开了一份 62 页的 PDF标题是《How the Ideas Came Together》。如果把它称为“OpenAI公开的核心手稿”甚至“完整思维链”就会把材料的性质带偏。更准确的理解是这是一组对发现过程的事后重构。文档摘要明确说明这些笔记由模型在阅读原始推理轨迹、最终论文和研究说明之后写成目标是重构证明思路如何逐步汇合。它关注的不只是成功路线也保留了重要的错误猜想、失败方案、反例和表示转换。资源我已上传: How the Ideas Came TogetherAI数学发现与证明路径重构手稿这使它非常适合技术精读却不能替代正式论文也不能直接当作未经整理的原始思维链Chain of Thought。对技术作者来说真正值得研究的问题不是“模型脑中到底想了什么”而是哪个数学结论被提出了哪条看似合理的路线为什么失败什么反例或不变量迫使研究者换一种表示最终结论由什么材料支撑读者怎样复核这也是本系列的写法不追逐“震撼”“泄露”之类的叙事而是逐章做数学调试。一、同一个结果为什么要看四类证据假设一篇文章写道“新的三对角递推给出了更强的二元码上界。”这句话至少有四个完全不同的问题。它是怎么被想到的这个命题精确说了什么小规模计算是否支持它它是否已经通过严格证明或机器检查一种材料无法同时回答这些问题。本系列为每个关键论断标注四类证据来源。标签回答的问题可以支撑什么判断不能替代什么Walkthrough想法怎样形成、哪里失败、为何转向发现过程与研究启发正式定理和完整证明Paper定义、假设、量词、定理与证明是什么论文中被论证的定理及其适用条件独立复现与同行共识Computation有限实例能否复算公式是否通过回归测试指定代码、参数和精度下的数值事实一般定理和渐近结论Formal/Review推理是否经过形式化验证或专家复核各自检查范围内的可靠性未编码的背景假设与研究价值判断这里把Formal和Review放在同一栏只是为了记录“主张还经历了哪些补充检查”并不表示二者提供同等保证。Lean、Coq 等系统检查的是已经编码的命题和推导专家复核则依赖审查范围、专业判断和公开讨论。后续文章会分别说明两者的状态。这里最常见的错误是证据“越级”。例如从“模型给出了一条有趣路线”跳到“定理已证明”从“随机测了 100 个样例”跳到“对任意输入都成立”从“预印本已经公开”跳到“结论已经形成学界共识”从“某个引理被 Lean 验证”跳到“整篇论文都被形式化”。技术写作的第一原则不是让结论听起来更大而是让每句话停留在它的证据能够承载的位置。二、这份 PDF 是什么又不是什么1. 它是一份基于多类材料的叙事性重构“重构”意味着读者看到的是有结构的回顾而不是按生成顺序保留的逐词元内部记录。它可能更清楚地突出主线也可能省略大量无效搜索、上下文交流和工程细节。因此我们可以从中分析发现模式却不应据此推断某个模型在某一分钟“真实地想了什么”。2. 它不是正式论文的替代品Walkthrough 可以说“先尝试全局范数再转向 Mellin 变换”但精确的函数空间、极限顺序、常数归一化和边界条件仍要回到论文。特别是在高维渐近、算术复杂性和算子代数中少一个量词或多一个正则性条件都可能改变命题。3. 它也不是一份统一难度的教材62 页覆盖的数学跨度很大球堆积和 Fourier 分析、编码理论、群与算子代数、算术复杂性、量子信息、格问题、凸几何以及极值组合。文档真正统一的不是学科而是一种研究节奏先用熟悉工具逼近问题发现某个信息被丢失构造反例或失败用例换到能保存该信息的表示再用独立检查闭环。三、12 章不是 12 条新闻而是一张方法地图为了便于阅读我把 12 章按主要技术对象重新分组。分类不是互斥的只是帮助读者选择入口。组别章节主题反复出现的技术动作调和分析与编码高维球堆积二元码的新谱方法Fourier/Mellin 变换、正核、Jacobi 算子、最小反例群与算子代数非 sofic 构造Connes 型刚性问题势函数、扩张性、可测结构、进位机制计算复杂性permanent积和式的算术电路下界算术公式下界GapCVP偏导数空间、秩、重构、局部一致性到全局赋值量子信息量子并行重复与 resolvent purification后选择、Born 权重、谱分解与纯化离散与凸几何Ehrhart 不等式与 jet counting消失阶数、多项式计数、几何与代数互译极值组合Ramsey 调色板构造紧致性猜想反例二退化图计数颜色复用、饱和矩阵、Hamming 宿主、熵势函数这张表也解释了为什么本系列不按 PDF 页码做逐段翻译。逐句翻译会得到许多名词却不一定看见技术动作。更适合 CSDN 的方式是每篇选一个可以精确定义的故障点给出代码或缩小模型然后再解释它如何通向正式证明。四、为什么“可纠错”比“一次答对”更重要OpenAI 的 Our First Proof submissions 页面提供了一个很有价值的现实案例OpenAI 起初认为第 2 题的证明尝试很可能正确随后根据题目官方评论和社区的进一步分析将判断更新为“不正确”。这个例子不应该被简单解读为“模型不可靠”或“模型已经是数学家”。它说明的是研究流程的本质候选证明可以由模型产生初始判断本身也可能出错反例、专家意见和后续复核可以推翻初始判断结论和公开材料应随新证据更新。官方在 Advancing science and math with GPT-5.2 中也明确指出当前系统不是独立研究者而是支持数学推理和早期探索的工具正确性、解释和背景责任仍由人类研究者承担。对于数学问题模型生成候选路线、扩写论证、交叉检查、专家复核和人工选择往往共同决定最终质量。这和软件工程很像。单元测试失败并不说明“编程没有价值”而是暴露了接口、假设或实现中的具体错误。数学反例也一样它不是研究的尴尬附录而是一种高密度信息。五、本系列如何写一个数学主张后续文章会尽量把关键主张写成“证据卡片”最少包含八个字段claim 要检查的精确主张 definitions 对象与参数定义 quantifiers 对所有、存在、充分大或渐近意义 baseline 已知构造或竞争结果 counterexample 最小失败用例 computation 代码、参数、输出与误差 paper_reference 正式来源 formal_status 形式化验证状态及专家复核范围配套脚本code/00_evidence_card.py不会验证数学它只做一件朴素但重要的事如果作者没有填满关键元数据就不要急着写结论。00_evidence_card.py代码如下A tiny metadata checker for mathematical claims. It does not verify a proof. It makes missing evidence explicit before a technical article is published. from__future__importannotations REQUIRED_FIELDS(claim,definitions,quantifiers,baseline,counterexample,computation,paper_reference,formal_status,)card{claim:The original Jacobi recurrence gives a valid upper bound.,definitions:n8, k1, L7; s1/2; even-parity binary code.,quantifiers:Claimed for every feasible code under these parameters.,baseline:Explicit feasible code size 128.,counterexample:Claimed bound 508/7, which is smaller than 128.,computation:wrong lambda0.75; corrected lambda≈0.5692891164.,paper_reference:How the Ideas Came Together, Chapter 2.,formal_status:Not checked in Lean; checked numerically and algebraically.,}defvalidate_evidence_card(item:dict[str,str])-list[str]:return[keyforkeyinREQUIRED_FIELDSifnotitem.get(key,).strip()]if__name____main__:missingvalidate_evidence_card(card)forkeyinREQUIRED_FIELDS:print(f{key:16}:{card[key]})print(f\nstatus:{INCOMPLETE: , .join(missing)ifmissingelsemetadata complete})运行方式python-Bcode/00_evidence_card.py用第 2 章“码长为 8 的二元码”案例填卡会得到以下核心信息claim: 原始 Jacobi 递推给出合法上界 definitions: n8k1L7s1/2对象为偶校验二元码 quantifiers: 对这些参数下的每个可行码都声称成立 baseline: 显式偶校验码大小 128 counterexample: 声称的上界 508/7严格小于 128 computation: 错误 λ0.75修正后 λ≈0.5692891164 formal_status: 未在 Lean 中检查已做数值和代数复核 status: metadata complete注意metadata complete只表示“字段齐全”不是“定理正确”。恰恰相反这张卡让矛盾变得一眼可见如果一个上界小于已经构造出的可行对象它就必然有错。六、同一句“错误递推”在四类证据里分别是什么下面提前预告下一篇的案例。在Walkthrough中我们关心的是发现顺序早期探索先把经典 Krawtchouk 递推类比到具有更高重数的调和空间算出结果后码长为 8 的反例暴露了问题检查随即回到算子的来源。在Computation中参数取n 8 n8n8、k 1 k1k1、L 7 L7L7和s 1 / 2 s1/2s1/2。把二元码字映射为单位符号向量后任意两个不同偶校验码字的 Hamming 距离至少为 2因此内积至多为1 / 2 1/21/2它确实是待检验上界的可行对象。此时构造一个7 × 7 7\times77×7的对称三对角矩阵错误递推的最大特征值为0.75 0.750.75相应上界为508 7 ≈ 72.5714. \frac{508}{7}\approx72.5714.7508​≈72.5714.但码长为 8 的偶校验码含有2 8 − 1 128 2^{8-1}12828−1128个码字因此这个“上界”当场失败。在Paper中仅指出失败还不够。正式证明必须从实际的添加/删除坐标映射出发推导正确的归一化、重数、正核和剩余 Gram 项最后得到合法的线性规划界。在Formal/Review中我们还要继续问哪些恒等式只是手算哪些矩阵正性经过了机器检查专家复核覆盖了哪些步骤是否检查了边界参数如果没有形式化证书就明确写“未形式化验证”而不是用“可验证”暗示已经完成机械证明如果只有专家复核也不把它等同于形式化验证。同一个故事经过四个视角才从“有趣的模型轶事”变成可审查的技术材料。七、写作和复现的具体规则为了避免系列在长篇公式中失去边界我会遵守以下规则。规则 1先写量词再写结论“在测试参数中成立”“对每个有限n nn成立”“当d → ∞ d\to\inftyd→∞时指数率成立”是三种不同强度的句子。后续每篇都会说明有限参数、渐近变量和极限顺序。规则 2一定给竞争基线漂亮的数值如果没有基线几乎没有解释力。编码上界要和显式码比较permanent 下界要区分算术电路与算术公式球堆积要区分线性规划方法的极限与真实的最密堆积。规则 3先找最小反例再跑大实验小参数的价值不是“玩具”而是便于枚举、精确算术和定位故障。一个n 8 n8n8的反例比画出n 10 5 n10^5n105的光滑渐近曲线更能诊断错误公式。规则 4把失败写完整失败路线不是一句“这种方法不行”而应回答它原本想控制什么量丢失了哪类信息反例怎样击中它新表示为什么保留了被丢掉的信息八、这份材料最值得学的不是“AI 灵光一现”精读 62 页之后我认为最值得写成技术系列的不是某个模型是否“像数学家”而是三种可迁移的研究习惯。第一把失败变成可计算对象。全局范数失效就构造具有相同范数、不同质量位置的剖面递推可疑就寻找最短的可行码。第二追问算子的来源而不是只看公式外形。两个三对角矩阵可能只差一个根号位置却对应完全不同的正交结构。形式相似不是结构同源。第三为结论设计尽可能独立的否证通道。一个候选证明如果只能由生成它的同一套直觉来检查就很脆弱。显式构造、精确计算、不同方法的交叉检查、专家审查和形式化证明提供的是不同方向的压力测试。下一篇我们就从最小反例开始在n 8 n8n8、k 1 k1k1、L 7 L7L7和s 1 / 2 s1/2s1/2时为什么一个看似自然的 Krawtchouk 型递推会给出72.57 128 72.5712872.57128这种不可能的编码上界修正它需要的不是调整一个常数而是重新找到三对角算子背后的关联映射incidence maps。证据边界Walkthrough本文对发现过程的描述来自How the Ideas Came Together的事后重构。Paper具体定理应以各章对应正式论文为准本文不替代论文证明。Computation证据卡脚本仅检查元数据完整性编码数值将在下一篇给出可运行复现。Formal/Review本文及配套脚本没有提供 Lean/Coq/Isabelle 证明证书文中的“数值和代数复核”也不等同于专家同行评审。参考资料How the Ideas Came TogetherOpenAIPDFOur First Proof submissionsOpenAIAdvancing science and math with GPT-5.2OpenAI