2026-08-26
在四字母Watson-Crick最大配对模型里，不含长度为1的螺旋、至多两条长度为2的孤立栈、且避开两种局部障碍的目标，被Lean核验证实可唯一设计。
RNA inverse folding问的是反过来的问题：给定目标二级结构，能不能找到一条序列，让这条序列在能量模型下唯一折成这个目标。真实热力学很脏。这篇用的是Haleš等人的四字母简化模型：只允许A-U和C-G，不许假结，相邻碱基可以配对，能量就是配对数取负。序列是design，当且仅当目标是它唯一的、配对数最多的无交叉折法。
Haleš的proper separated coloring已经是一张设计证书：局部端口不冲突，再加上灰对和未配对A的level错开，就能保证唯一最大配对。Boury等人把level做成模m的有限状态，并证明所有螺旋长度至少为3、且避开m5和m3•两种局部障碍的目标，都能在线性时间里给出模2着色。长度2的孤立栈少一个可切换的内部位置，这条「全长螺旋」保证到这里就断了。
新结果是一张资源计数归纳，不是新的局部着色单词。把目标看成区间树，每条最大螺旋是一条颜色单词，B/W/G分别规定G-C、C-G和A-U取向。模2下未配对点走residue ξ，灰对走相反的η。长度为2的螺旋转移表只有有限几种：例如η→η时若上头还要求灰头，唯一单词是GG，出口也只能是灰。两个子树如果都已经占用了目标里仅有的两条孤立栈，入口螺旋就不可能再是长度2，于是至少长度3，可以改用Boury表里已经发表过的非灰收尾单词GBB或GWW，环上的暴露从三个G变成合法的{W,G,B}。
归纳对无孤立栈的子树给出可行入口状态集合F，对至少含一条的子树给出较弱的Q。构造是自上而下、确定性的，给出具体序列，再沿用Haleš的计数加唯一性，证明任何别的兼容折法配对数都更少。
完整定理RNA.atMostTwoShortHelixDesignability在Lean 4里形式化。冻结源在隔离容器里从零重建：46个文件、20,738行、1,616条声明（含1,102条定理），Lake跑3,070个任务、894.10秒。传递公理集只有propext、Classical.choice、Quot.sound，没有sorry。另用一份匿名数学规格加一份全新的Claude Code会话做盲审，结论是faithful and complete。ChatGPT、Codex和Claude Code贯穿选题、证明、Lean和写作，人类作者拍板并担责。
定理给出的是充分条件，不是刻画面。每个避开m5和m3•、没有孤立碱基对、至多两条孤立栈、其余螺旋长度至少3的目标，都有模2分离着色，因而在这个模型里可设计。三条孤立栈的例子可以没有proper的模2着色，但作者展示的那个目标仍有普通分离着色并且可设计，所以「两条」是这套构造的资源上限，不是可设计性的结构边界。
算法含义同样收着说。Boury的动态规划对固定m已经是线性时间判定加构造，这篇没有改进一般复杂度，只保证在K≤2类上模2过程不会报不可分，并给出不搜整张状态表的显式自上而下证人。着色算法在树和最大螺旋显式存储时也是线性时间。
对做形式化数学和AI辅助证明的人，这是一份把生成式模型用到可复现形式化终点的公开记录：内核验收、隔离重建、公理审计、盲审规格对照，一层一层排好，不把多模型同意当成证据。对RNA设计，它把Boury的全长螺旋保证往短螺旋方向推了一步，并给出可当逆折叠软件测试基线的确定性序列。它不是Turner能量下的设计器，作者自己把这点写死了。
模型排除G-U wobble、假结、堆积能、环熵、离子、系综目标和三维约束，最小弧长θ=0。避开m3•在生物学上很窄：带两个以上分支螺旋的非根环不能有未配对碱基。手稿和形式化在发布时还没有完成独立人类专家审稿，盲审也是AI对AI。作者写明内核检查不证明生物学真实性、新颖性或模型外的正确性。文献检索截至2026年8月19日，作者说不能当作新颖性证明。三条及以上孤立栈何时仍可着色，是文中明确留下的问题。