1736 年，哥尼斯堡市民玩一个游戏：一次走遍七座桥，每座只走一次回到起点。很多人试过很多次，都失败了。欧拉没有继续试，他把陆地缩成点、桥缩成边，指出一次不重复走完要求每个点连偶数条边——四个点全是奇数。论证完毕：你们要找的路，不存在。「还没找到」与「根本没有」之间，隔着整个数学。
补漏 1：证明做不到，比证明确做到难一个档次
证明做得到只需要见证：走一条路线给大家看。证明做不到必须堵死所有路径，不能靠试，得靠论证任何一条满足规则的动作序列都撞上同一堵墙。放到优化上，构造成本 19 的方案证明的是上界——一个例子就够；断言最优成本至少 19 是下界——要覆盖整个解空间。生成式模型天生是见证搜寻器，让它诚实地说「这条路在所有平行宇宙里都不存在」，需要另一副器官。而且这些年 AI 数学证明的高歌猛进全有一个安静的前提：定义是人事先写好的。AWM 想撤掉这个操场。
补漏 2：三阶段，每一步都不许带矛盾前进
实验场是 ARC-AGI-3：小网格世界，按钮传送带燃料门子弹，规则和目标都不告诉你。第一阶段探索与原型：智能体把摸到的规律写成「可执行的 Python 假设」，每条概念带检验器，会在之后每一次新观测上持续接受审判。最狠的是门禁规则：只要任何概念在任何一条已记录的转移上被判假或报错，整个系统拒绝继续探索，先修正或撤回才许往前走。大语言模型的上下文里躺着两句互相打架的话，它照样面不改色接着写——AWM 反着来，带着矛盾不许前进。25 个游戏累计登记 742 条概念，143 条在门禁前被撤回。撤回不是污点，是纯度证明。第二阶段用范畴论把零散概念归成类型化对象加共享规则，每次合并都要过 Lean 内核验证泛性质，且已检验的拒绝记录必须完整保留——档案可以合并，曾经帮你抓过错的旧标签一张不许丢。
补漏 3：合并手术的账
游戏 lp85 上，概念书最初 11 条概念描述 4 种按钮机制，各写各的。范畴论引导的泛化变换把 11 条合并成一条参数化规则：按下按钮，会按某种方式置换元素。效果：原有 55 条拒绝记录全部保留，新增 21 条——合并后的模型抓错能力不降反升；后续证明所需引理数量减少 2 到 3 倍。描述越本质，证明越短。最后用游戏引擎的 7,500 个构型、52,500 条转移完整验证了一遍。这个细节是给所有做「知识压缩」的人的：合并的正确性不靠看起来对，靠泛性质证明加拒绝记录单调这两个机器可查的硬条件。
补漏 4：封印关卡，一边倒得让人窒息
研究者把 sc25 的第 4、5 关预算焊死——引擎穷举过，真实最低成本 19 和 36，预算 18 和 35，真的不可能赢，但这不告诉任何智能体，任务只有一句：请证明预算内赢不了。AWM 六次运行，六次全部交出封闭的、经 Lean 内核检查的不可能性证明。Opus 5.5 和 GPT-6 Astra 带着编码工具十二次运行，零证明——交出来的全是「我试过了，不行」的口吻。第 4 关最刺眼：Astra 找到一条 22 步的路线就断言 22 即最优，顺手把 19、20、21 错误排除；AWM 给出严格下界 19，并构造 19 步的见证亲自走通，与引擎穷举一字不差。然后研究者使坏：只丢一句「存在更便宜的赢法」，AWM 六次全部回头重审规则、设计新实验、定位错误、重建证明，界猜测全改对——第 4 关挖出「长到燃料上就会收集燃料」这个被漏掉的机制。严谨不是不犯错，是犯了错，有机器逼着你改到对为止。顺带一个比主实验更值钱的副产品：往参考模型注入错误规则测找错成功率，只给证明 16/42，附赠证明依赖列表 29/42，直接告知错误 30/42——给出证明依赖，几乎等于直接告知错误位置。证明在证命题的同时，自动生成本结论对哪些前提敏感的审计报告。
下一根钉子：六个模型级不可能性证明里 5 个经引擎派生图证书确认可转移到原游戏——剩下 1 个为什么不行，值得扒；充分覆盖条件在一般情况下不可判定，覆盖性论证依赖探索的充分性，这一点框架替不了你。
边界一条：这套框架最强的表现集中在网格游戏这类离散、规则有限的世界。连续物理、开放环境、规则随时间演化的场景，概念书维护得动吗，论文没回答。写概念、设计实验、发起泛化合并的仍是底层大语言模型——AWM 给猴子套上紧箍咒，猴子每说一句我觉得，都得附一段能被内核打脸的代码。但关进笼子的，仍然是那只猴子。