LLM 让 Lean 证明自动化成为现实

We have proof automation now

我一直对 Rocq 和 Lean 这类依赖类型语言情有独钟，它们能将微妙的不变量编码进类型系统，避免团队协作中的理解偏差。但过去，强大的类型系统意味着巨大的证明成本，像 seL4 项目那样，证明代码量是 C 代码的二十倍，耗时更是设计实现的十倍。F* 等尝试用 SMT 求解器自动化，却常陷入不可预测的等待，迫使开发者像侍奉神灵般揣摩求解器喜好。如今，LLM 的出现结合证明无关性理论，让证明自动化变得极具潜力。我尝试用 Lean 编写了一个 Zstandard 解压缩器，发现 LLM 能有效规避类型检查器崩溃，让依赖类型系统突然变得实用。Zstandard 凭借 FSE 熵编码器在压缩率和速度上超越 gzip，而 LLM 或许能让我们不再为繁琐的证明工程而头疼。