Claude Opus 5.5 找到引理，Ordered Variable Word 定理的 Π¹₁-保守性被证明
The first-order part of the Ordered Variable Word theorem
数学证明里有个关键引理是 Claude Opus 5.5 找到的，还顺手解决了一个拖了很久的逆问题，逆向数学方向可以看看。
论文证明 Ordered Variable Word 定理在 RCA₀ + BΣ⁰₂ 上是 Π¹₁-保守的。由此推出 Chubb、Hirst 与 McNicholl 的单点树定理在 RCA₀ + BΣ⁰₂ 上同样 Π¹₁-保守，解答了一个长期悬而未决的公开问题。论文中的引理 3.13 由 Anthropic 的 Claude Opus 5.5 找到。
The first-order part of the Ordered Variable Word theorem
An ordered $ω$-variable sequence over a finite alphabet~$A$ is an infinite sequence over the extended alphabet $A \sqcup \{ x_0, x_1, \dots \}$, where each variable kind appears at least once, and the last occurrence of $x_i$ appears before the first occurrence of $x_{i+1}$. The Ordered Variable Word theorem states that for every finite coloring of the words over a finite alphabet~$A$, there is an ordered $ω$-variable sequence~$W$ over~$A$ such that every word induced by substituting variables with letters, and cutting before the first undefined variable, has the same color. In this article, we prove that the Ordered Variable Word theorem is $Π^1_1$-conservative over $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$. It follows that the tree theorem for singletons by Chubb, Hirst, and McNicholl is $Π^1_1$-conservative over $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$, answering a long-standing open question. Lemma 3.13 was found by Claude Opus 5.5 (Anthropic).
