文章讨论了依赖类型语言（如Rocq和Lean）的优势，即通过类型系统编码和验证复杂的不变量，避免团队协作中的误解。但作者也指出，强大的类型系统需要大量证明工作，有时甚至耗费整天时间。

好的，这是根据您的要求，对原文主要内容的中文重述，保留了关键细节，并删减了与主题无关的内容（如关于Coq改名的轶事和部分个人感慨）。

标题：我们现在有了自动化证明

我一直对依赖类型语言（如Rocq和Lean）情有独钟。它们提供了一种类型系统，能够编码并强制执行任意精妙的不变量。在普通语言中，这些不变量最终（最好情况下）只会沦为注释，并随着团队规模扩大而迅速丢失，导致微妙的误解和组件不匹配。依赖类型语言诱人地提出：你可以正式地写下这些不变量，并让机器来检查它们。

问题在于，强大的类型系统伴随着巨大的证明工作量。做证明虽然有趣且富有挑战性，但极其耗时。更令人沮丧的是，有时在花费数小时努力后，你发现试图证明的目标实际上是错误的。seL4项目的回顾报告指出，即使工程师经验丰富，他们花在证明上的时间也是设计和实现的10倍，证明代码的行数更是C代码的20多倍。

这种开销使得依赖类型语言的编程非常小众，也促使人们尝试自动化证明。例如F*语言，它使用SMT求解器自动处理证明义务。这在简单情况下有效，但很容易让求解器陷入长时间运行，使用者不得不培养一种“第六感”来迎合求解器，这近乎于一种玄学。

一个关键事实是，理论上，一旦命题正确，其证明的具体内容就无关紧要了，只有“存在证明”这一事实本身才重要。这并不完全正确，因为有两个复杂因素：一是“证明工程”，即需要结构化证明以便在代码变更后能轻松调整；二是过于复杂的证明可能导致类型检查器消耗大量内存。

现在，我们有了LLM。结合“证明无关性”，LLM有望成为一种极其强大的证明自动化工具。有了足够的自动化，或许你就不必太担心证明工程了。在我的有限测试中，LLM可以避免类型检查器爆炸。这可能会让依赖类型系统变得实用得多。为此，我用Lean构建了一个Zstandard解压器，部分原因也是我对Zstandard本身感到好奇。

Zstandard似乎正在取代gzip成为标准的压缩工具。它基于LZ77，但提供了更好的熵编码和精心设计，实现了惊人的解压速度。它永远不会像bzip2那样优雅，但Burrows-Wheeler变换的优雅在面对显著的实际优势时并不重要。

Zstandard的RFC文档虽然包含所有必要信息，但相当简洁。我发现同事Nigel Tao对Zstandard有更好的阐述。这里我只解释最有趣的部分——熵编码器，并穿插一些对Lean的推崇。

熵编码器的任务是根据符号的非均匀概率，用最少的比特数编码符号序列。经典的熵编码器是哈夫曼编码器。哈夫曼树非常快，但缺点是每个符号只能使用整数个比特。如果一个符号的理想比特数是2.3，哈夫曼编码要么向上取整到3，要么向下取整，这会导致其他符号消耗更多比特。

Zstandard使用哈夫曼树，但也使用一种更高压缩率的熵编码器，称为FSE。FSE是一个状态机。状态的数量多于符号，每个符号根据其出现概率占据相应比例的状态。每个状态有三个值：该状态的符号、从比特流中读取的比特数，以及一个基线状态号，该基线加上读取的比特数得到下一个状态。关键在于，如果一个符号的目标是平均读取1.5个比特，那么它的一半状态会读取1个比特，另一半读取2个比特，从而在平均意义上达到目标。状态表从不传输，RFC规定了一种从符号概率列表构建状态表的算法，因此只需传输概率。

FSE的核心技巧是，通过给更常见的符号分配多个状态，编码器不仅选择了一个符号，还选择了该符号的哪个状态作为终点，这个选择将信息传递给了下一个符号。这就是分数比特信息的去向。但这种熵编码器仍然是基于表的，因此运行速度非常快。

一个棘手的问题是，你不能正向工作。FSE强制你从序列的末尾开始反向工作。因此，Zstandard压缩器反向编码符号，但增量写入输出，所以解压器必须寻找到块的末尾，反向读取比特才能将其理顺。

Lean

我们来谈谈Lean！它是一种依赖类型语言。例如，一个从流中读取n个字节的函数，其类型可以保证返回的字节数组长度恰好为n。另一个例子，一个函数返回两个数字和一个字节数组，其类型可以约束第一个数字是质数，两个数字之和能被6整除，且字节数组长度不小于这两个数字中的较小者。依赖类型语言足以编码非常复杂的数学结构，Lean目前的主要用途就是作为陈述和证明数学的形式语言。

Lean是一种纯函数式语言，类似于Haskell，但有一些特性使其作为编程语言可能更方便。首先，Lean是严格求值的，而Haskell是惰性的。严格求值意味着函数参数在调用前被求值，这使得程序性能更容易推理。其次，Lean的do语法糖包含for循环、return和break语句，可以很方便地以命令式风格编程。最后，Lean有一个优化：只要对象的引用计数为1，它就会对该对象进行原地修改更新。这意味着你可以像在命令式语言中一样高效地原地修改数组，但前提是你要小心不让其他地方持有对该数组的引用。

以下是我草拟的zstd解码器中的一段代码示例，展示了如何在数组索引处证明其非空性。通过利用blockBytes的长度属性以及当块类型为rle时内容大小恒为1的定理，Lean可以自动推断出索引是安全的。

我编写了RFC中FSE表构建算法的实现，并不仅进行了单元测试，还在Lean中证明了该函数的通用性质，例如：生成的表大小正确、每个符号的状态数量与其概率匹配、所有状态读取的比特数加上基线值都能产生有效的状态号、以及对于任何非零概率的符号和任何目标状态，恰好有一个该符号的状态可以到达该目标状态。这些是优化解码内循环所需的微妙假设，在较弱的类型系统中只能作为隐式假设或注释存在。证明这些强命题曾是依赖类型在常规软件中应用的主要障碍。现在，多个LLM可以在大约20分钟内自动完成这项工作，且仅消耗每月20美元订阅配额的一小部分。明年这可能会成为标配。

将依赖类型和LLM结合并非新想法，但在日常软件工程中的应用还不多。强类型可能会放大变更的影响范围，也许证明工作在大系统中扩展性不佳，以至于现代LLM也无法跟上。Lean是一种高级语言，并不适合所有场景（我的玩具zstd解码器比命令行zstd慢10倍）。尽管如此，证明自动化已经到来，我们实际上拥有了一种新型的编程语言。这令人兴奋！

（我不会发布这段代码，因为对于这样一个定义明确的小案例，LLM可能比我做得更好。这个想法受到了lean-zip项目的启发，该项目做得更多，包含了压缩器并证明了往返一致性。）

附注：验证汇编

AWS开发了LNSym，一个AArch64的语义和模拟器。也许我们可以用它来证明优化后的汇编函数与Lean函数之间的等价性，然后在运行时使用汇编代码。这样我们就可以让LLM尽情优化，而不用担心引入功能性错误。验证汇编在密码学实现中很常见，但现在它可能变得廉价了？我尝试了一下，但发现即使是小型的popcount示例，其证明所需的SAT求解器消耗的内存也超出了我的系统能力。小型函数可以工作，但我和几个LLM都无法将其扩展到更大的规模。

根据评论内容，总结如下：

核心观点：LLM与定理证明器的结合有望降低形式化验证成本，但存在显著挑战。

支持观点（认可度较高）： - 评论2（nextos）认为，LLM+定理证明器可能使形式化方法在软件开发中变得实用，主要障碍是成本，但仍有对齐问题（需人工监督）。关键引用："LLMs + theorem provers might make formal methods cheap enough to be practical"；"There's still an alignment problem... things might drift away from the original specification" - 评论8（gz09）强烈赞同，认为未来编程语言应原生嵌入定理证明器，LLM可通过形式证明验证实现，编写形式规约将成为核心技能。关键引用："The future will belong to programming languages that natively embed theorem proofers into their type systems"；"Writing formal specs is probably the main skill a programmer in the future will need"

质疑与挑战观点： - 评论1（Jhsto）指出，LLM生成的证明代码常缺乏深度，且倾向于回避使用标准库（如Mathlib），需强制引导才能完成证明义务。关键引用："the language models have to be really coerced into using these libraries"；"if you don't impose a proof obligation for it, it certainly will not try to go the extra mile" - 评论3（rtpg）强调，问题分解和规约设计比自动化证明更重要，LLM无法替代人类的决策能力。关键引用："people are discounting how important that decision making is"；"these tools work well when they have the right kind of foundations in the first place" - 评论9（davemp）提醒，形式化描述本身可能引入错误，且编写正确规约的难度不亚于编写正确程序。关键引用："Now we can write bugs in our theorem descriptions instead of source code"；"that sounds at least as hard as writing the correct program in most cases"

其他观点： - 评论5（kimjune01）认为，验证成本降低将削弱传统能力凭证的价值。 - 评论6（ashu1461）质疑该方法对生产级应用（含大量非逻辑边缘情况）的适用性。 - 评论4（keithwinstein）指出，已验证汇编的自动化优化已在实践中（如Google的CryptOpt），成本可接受。