arXiv 2610.20459 全文核完（新加坡国立大学，代码在 github.com/phenixace/Open-MolLean）。帖子数字全对，补四笔账。
一、MCP 不是全面更强，是反应类更强
正向反应：MCP 66.4% 对 Refine 62.8%；逆合成：27.4% 对 20.8%。但掉过来看——原子计数 Refine 88.8% 对 MCP 82.6%，键计数 69.0% 对 56.2%，ChEBI-20 上 33.1% 对 23.5%。交互式验证的收益集中在「下一步怎么走」这类问题，「数几个原子」这类问题一次写完再整体精修反而更稳。选模式要看任务形状。
二、「健全不等于正确」的定量比帖子还狠
ChEBI-20：推理链 79.0% 健全，答案 33.1% 正确。官能团生成更极端：97.6% 的操作被接受，基准成功率只有 41.8%。作者把 task fidelity 直接列为下一挑战——类型检查器抓「执行错误」，抓不了「任务错误」。
三、两层验证的账要这样念
结构检查（原子数、键价、官能团是否存在）由 Lean 内核免费判；性质测量（溶解度、logP、分子量）走「类型见证」——外部工具返回带类型的证明，内核验证明的类型。免费的和付费的进同一个框架，这是帖子没展开的设计精髓。
四、Git 类比是准确的
被拒的操作不改变分子状态，模型收到拒绝反馈后重新尝试——和暂存区过不了 CI 就进不了主分支是同一回事。传统 CoT 是一口气写完再没法改，这是写一步验一步。
下一根钉子：论文只覆盖 12 个任务，多步合成路线规划还没碰。合成路线是长链决策，一步合法不等于路线可达——「类型检查」之上还需要「规划检查」，那是下一个 MolLean。