OpenAI 撤回的 Weil 类论文被 2b4m 形式化验证：符号错误被定位到 §3.4

openai-wiles — 被撤回的 Weil 类手稿，以两种方式形式化

OpenAI 被撤回的预印本 "Algebraicity of Weil classes on split abelian eightfolds" 的 2b4m 形式化（撤回前 PDF、 撤回通知）。

2b4m 是什么，以及为什么这可以手工检查

2b4m（"too big for margin"，源自费马）是一个基于不寻常前提设计的证明 检查器：证明不期望由人类编写，但期望它们对人类的检查极其容易。它正是为本目录所处的情形而构建的——一个机器生成的论证，需要有人来审计。

有三个设计选择对阅读以下内容很重要，而且它们都不需要你先学习这门语言。

证明是显式命名的步骤。每一步都完整陈述其公式，并指明规则 以及为其提供依据的先前步骤。没有证明搜索，没有隐藏上下文，没有默默做三件事的 策略。写出来的正是检查器所检查的：

theorem theExtraObjectIsNotAScalarGraph: not isAScalarGraph(theExtraObject)
proof
  @given-it-were-a-scalar-graph |
    assume isAScalarGraph(theExtraObject) {
      @it-is-a-scalar-graph |
        isAScalarGraph(theExtraObject)
        [by hypothesis given-it-were-a-scalar-graph]
      @then-it-annihilates |
        pair(theExtraObject, exceptionalPart) = zeroPairing
        [using specialize aScalarGraphAnnihilatesTheExceptionalPart(theExtraObject)
          it-is-a-scalar-graph]
      @but-it-detects |
        pair(theExtraObject, exceptionalPart) != zeroPairing
        [by cite theExtraObjectDetectsTheExceptionalPart]
    }
  @conclusion |
    not isAScalarGraph(theExtraObject)
    [by not_intro given-it-were-a-scalar-graph then-it-annihilates but-it-detects]
qed

这就是整个证明，逐字来自 detection/nonpolarization.md，你可以按它的本来面目阅读它：假设它是一个标量图；那么它湮灭例外部分；但它 检测到它；矛盾。步骤标签 就是论证的大纲——2b4m query outline <file> <theorem> 只打印那一列。 连接词是单词（and、or、not、->、iff），每个名称都可 grep，并且 诊断信息会向你回引表面语法。没有证明助手经验的数学家应该能够跟随它并提出异议。这就是设计目标，也正是这次审计值得发表、而不仅仅是断言一个结论的原因。

引入借来的事实只需一行。对论文架构的形式化并不想重新发展 Hodge 理论或 Floer 同调——它想假设所引用的结果 并检查它们如何组合。在 2b4m 中，这种假设是一等声明：

hole remmertProperMapping
  cites "Grauert-Remmert, Coherent Analytic Sheaves [15]: proper mapping theorem":
  forall h: AnalyticSpace; isProperOverTheBase(h) -> isClosedAnalytic(imageInTheBase(h))

一个 hole 是未证明的步骤。一个被引用的洞是基于外部权威假设的： 检查器仍然将其视为假设，仍然列出它，并在每次运行时打印其定位符—— 但它不会阻止严格检查，因为证明检查器唯一不能做的事情就是 确认 Grauert–Remmert 说了那一行所声称的内容。一个未被引用的洞确实会阻止。因此 假设集始终可见且始终有归属，你可以通过阅读 36 条单行引用而不是信任一个 5,000 行的开发来审计形式化。

有意地，axiom 保留给理论自身的原语（这里是 𝔽₂ 的环律），而 axiom ... cites 是硬错误——因此借来的定理不能被悄悄重新标记为 局部公理，否则未证明的步骤就不再可见。

那么，策略是：公理化接口，形式化架构。论文 引用的，我们引用。论文声称证明的，我们证明——如果它不成立， 检查器会指出该步骤以及所有依赖于它的内容。

运行检查

你需要构建 2b4m 检查器，并让 B4M_STD_DIR 指向其标准库（其中使用了两个文件：std/integer.b4m 和 std/complex.b4m）。

git clone https://github.com/ityonemo/2b4m && (cd 2b4m && zig build)
export B4M_STD_DIR=$PWD/2b4m/std
export PATH=$PWD/2b4m/zig-out/bin:$PATH

2b4m check architecture-right.md theWeilPlaneIsSpannedByAlgebraicClasses   # OK
2b4m check architecture-wrong.md theWeilPlaneIsSpannedByAlgebraicClasses   # error at Lemma 3.6
2b4m check signs.md                                                        # Section 6's signs
./diff-chains.sh                                                           # what differs

将 --axioms 添加到任一根目录，以打印带有每条引用的完整假设集。

它作为两条链存在，二者恰好在一个数学输入上不同——§3.4 的反向 稳定化迹符号——并将这一差异一直运行到定理 1.1。

2b4m check architecture-right.md theWeilPlaneIsSpannedByAlgebraicClasses  # PASSES
2b4m check architecture-wrong.md theWeilPlaneIsSpannedByAlgebraicClasses  # FAILS

运行 ./diff-chains.sh 以查看差异。六个文件重复；四个仅在 一行 import 上不同。数学恰好在两处出现分歧：traces-*.b4m 的符号公理 和 stabilization-traces-*.md 的算术。

两条链都无法判定哪个约定是正确的。 [6] 在其自身约定下 赋予 I(G₂) = (−1)^k = +1；通知断言该指标与手稿的 带符号双点计数之间存在不匹配——而非 [6] 内部的错误。裁决它意味着比较两种 定向约定，而这在此处尚未形式化。这一对所能确立的是：这个 符号是关键：§3.4 以上的一切都经过内核检查且对它无感，而 §3.4 本身则由它决定。

撤回通知所说

该证明在用于获得负双点的稳定迹论证中包含一个符号错误。 在手稿的带符号双点约定下，将 I(f₁) = −m 写作 m > 0。该证明为每条反向稳定迹赋予符号 +1，因此声称 插入 m 条这样的迹会使带符号计数为零。

考虑到标准尖点两个分支的相反源定向， 在此约定下每条反向迹的符号为 −1。因此所得计数为 I_new = I(f₁) − m = −2m ≠ 0。

此步骤所援引的 Eliashberg–Murphy 消去定理要求带符号双点 计数为零，因此其假设不满足。

-wrong 链就是那一段，经过机器检查。

布局

第 6 节的符号代数检查无误

论文的五个符号断言独立于迹问题得到验证。五个 全部有效——因此缺陷不在第 6 节。

• Lemma 6.2 的置换坍缩——四个行列式线交叉求和为 A + (pz + C)R，然后到方程 (6.3)。在所有 16 个 𝔽₂ 角上经过内核验证 （theCrossingSignsCollapse 在 signs.md 中）。
• Lemma 6.2 的第二步——在 l = i − 1 下从 A + (pz+C)R 到 (6.3)；在其八个奇偶性的所有 256 种赋值下均有效。
• Lemma 6.4 的循环符号——对元数 2 到 6 穷举；无不匹配。
• 第 6.2 节将 (6.8) 归约为 v + w + c + (c+q)(v+w+1) + (v+w)(c−1−q) + q = 0； 在所有 16 种赋值下均有效。
• Lemma 7.4 的相交符号——横截点处的局部符号为 (−1)^|x|。 定向差异的指数为 |x| − n，拼接贡献 (−1)^(n(n−1)/2)，而在 n = 8 处这些复合为 (−1)^|x|。有效——并且论文标记了 其自身的维度敏感性（“因为八是偶数”）；同样的论证在 n = 9 处为假。

两个观察解释了符号错误如何在这种检查下存活：

1. §6.2 说 "我们在不指定裸符号的情况下检查这一抵消。" 验证符号差异而非绝对符号，正是全局 +1/−1 翻转能通过每一项局部检查的原因。
2. 从被引来源引入的约定，对于任何依据引用论文对该来源的表述来公理化的形式化而言都是不可见的——它继承了它本应检测的那个错误。

假设

每一个未证明的步骤都是一个携带引用的 hole，因此严格的 check 在打印每个定位符时通过：

2b4m check --axioms architecture-right.md theWeilPlaneIsSpannedByAlgebraicClasses

36 个被引用的空洞，取自 arXiv:1303.0588v2 和 arXiv:1303.0586v1、Fulton [14]、Grauert–Remmert [15]、Grothendieck [16]、Milne [20]，以及引用的手稿行。唯一的 axiom 是 parity.b4m 中的 𝔽₂ 理论——一个理论自身的原语——加上一个谓词定义。引用不是验证：检查器无法确认某个来源确实说了定位符所声称的内容，这就是它打印出全部内容而非保持沉默的原因。

这也是一次 LLM 辅助证明写作的练习

该形式化是用 LLM 编写的，而该目录同时充当了对 2b4m 在此方面人体工学的测试：为了让机器编写的审计可信，该语言必须使哪些事情变得困难。

最尖锐的发现来自一次失败。在此过程中，审计产生了一个错误诊断——即 §3.4 是循环的，因为 [6] 据称仅当目标链接是松散的时才授予 +1 反向迹符号，而 §3.4 将松散性呈现为该步骤的输出。检查器似乎证实了这一点。它错了：松散性假设是被发明出来并归因于 [6] 的，而阅读引理 3.4 的证明（而非仅其陈述，其中符号未被赋值）表明松散性门控的是失稳迹 G₃/G₄，而非反向迹 G₂。一条带有自信注释的假公理永远检查为绿。

由此产生了两个变化，而两者正是这个版本值得一读的原因：

• hole … cites "<source>"——上文描述的机制。在它之前，axiom 意味着"理论原语"，hole 意味着"严格检查拒绝此"，因此从文献借来的结果没有诚实的归宿，并不断被写成局部公理以使树变绿。现在，借来的事实是一个通过检查同时保持披露的空洞，裸空洞仍然失败，而 axiom … cites 是硬错误，因此逃生舱口无法被重建。
• 提示规则现已写入 2b4m 的速查表 的 "THE AXIOMATIZATION RULE" 下：对于任何你无法引用的内容，首先写 hole，绝不要先公理化再审计；从参考文献本身而非引用它的论文来公理化参考文献；并且在从绿色树得出任何结论之前，检查有争议的输入是否是承重的。最后一条在此处捕获了一个真实的假阴性——第一次对正确/错误划分的尝试在两个符号上都通过了，因为迹计数被定义为一个常量。

实测数据，供任何想要校准此类输出可信度的人参考：在写完公理之后审计它们，在 29 条中捕获了 4 条违规——而修复这些违规的那一轮又引入了 5 条。自我审查不会收敛；拒绝继续的机制才会。

注意事项

• §3.4 不是循环的，且 reverseTraceSign 不携带松散性假设——见上文。手稿的步骤如所引用那样是可靠的；争议仅在于符号的值。
• 第 4–11 节的辛拓扑尚未验证。这些章节是此处若干引用输入的来源（anAlternatingChernCharacterIsAlgebraic、§10 的欧拉配对恒等式），而形式化则直接采信了它们。
• 被形式化的是架构：从 §12.4 往下的定理 1.1，加上 §3.4 的计数。而非 Hodge 理论或 Floer 理论的机制。