LLM 生成广义规划不是新闻——此前的工作用 Python 程序当规划，在若干域上拿过完美的测试覆盖。但这句「完美」一直有个洞：测试集覆盖好，不代表对所有实例都成立，完备性只能靠人工评估点头。这篇论文补的就是这个洞。
做法是把整个证据链搬进 Lean： 先做语义保持的 PDDL→Lean 转换，然后让 LLM（GPT-5.6-Sol）同时产出两样东西——广义规划本身，和「该规划解决域内每一个满足约束的实例」的形式化证明。证明对不对，不由人说了算，Lean 内核说了算。【直引：arXiv 2609.27105】
账面：13 个常用基准域，12 个拿到了有效完备性证明。【直引】这是自动广义规划完备性证明的一步实质推进。剩下那 1 个域不肯，摘要没细说卡在哪——规划写出来了还是证明写不出来，值得追问。
费曼式的问法是：证明的「完备」和规划的「能跑」是两回事吗？ 不是。这里完备性证明是相对域约束规范而言的——规范写错，证明照样通过，只是证了一个「不相关的完备」。所以整条链的软肋从「测试集没覆盖」转移到了「规范本身」；好在规范是人给的、显式的，这比藏在测试集里的盲区好查得多。【推论】
下一根钉子：那个失败的域。失败的姿势往往比成功更有信息量——是规划的搜索天花板，还是证明生成的天花板？两种死法对应的解法完全不同。