FRI (and friends) 使用 Lean4 形式化验证 FRI（及相关内容）

如果你不是专家，如何阅读密码学论文

Alice 写了一篇密码学论文。Charlie 不是专家。Charlie 怎么能确定这篇论文没问题呢？

Alice 可以请专家 Bob 审查她的论文。Charlie 可以依靠 Bob 的声誉来对 Alice 的论文获得一些间接的信心。我们能做得更好吗？

有一个叫做 Lean 的工具。与 Bob 不同，Lean 不是专家。但它会不断提问，直到它在内部完成一个严谨的、小步的数学证明。结果可以发布在 GitHub 上。通常这被称为 Lean 证明，或者证明的 Lean 形式化。

因此，在 Lean 的帮助下，也许 Charlie 不需要完全依赖 Bob 的声誉。

哪些内容被形式化了

去年十月，我的同事 Nico 在这里发表了 为什么 FRI 有效？。 这篇文章描述了他与合著者共同撰写的论文的精髓：

Albert Garreta (Nethermind Research), Nicolas Mohnblatt (zkSecurity), and Benedikt Wagner (Ethereum Foundation) 的 "FRI 的简化逐轮正确性证明"。

现在 它已经在 Lean 中被形式化 了，除了一个从 WHIR 论文 中引用的关于相互关联参数的结果。这个形式化主要由 Harmonic 的 Aristotle 和 Claude Code 完成。

该 存储库 包含了论文中定义和定理的 Lean 代码，包括证明。Lean 类型检查器确保这些定理是可以证明的。唯一可能出错的地方是错误形式化：Lean स्टेटमेंट 可能与论文中的 स्टेटमेंट 不完全对应。我需要在 Lean 和纸上运行一些例子，以完全确定形式化的正确性。相反，我只是将 Lean 代码与原始论文进行了比较。论文和形式化之间存在一些非关键的差异。

• 形式化增加了一个条件，即初始度数大于零。然后用它来表明求值域是非空的。我不确定是否真的需要这个额外的假设。这在实践中并不重要。
• 形式化证明了完美的完备性，这不是论文的主要主题。完备性结果让我确信，形式化没有意外地创建一个拒绝一切的验证器。
• 相互关联参数的定义一直在更新和稳定。该形式化基于截至 2025 年 12 月的论文快照。我正在监控作者的更新以及 Arklib 的选择。

说实话，我并没有期望找到严重的缺陷。实际上我没有发现任何缺陷。该论文的致谢提到 Ariel Gabizon 在早期草稿中发现了一个错误。这让我对论文的正确性充满信心。

Lean 形式化的优势在于证明的正确性不依赖于某人的严谨性。此外，这篇论文的形式化可以用作验证器实现的规范。

过程如何

ItaLean 2025

我参加了一个名为 ItaLean 2025 的研讨会。在研讨会之前不久，有一些关于使用人工智能代理将论文进行形式化的公告。我请 Nico 提出一些需要形式化的建议。他建议了他的关于 FRI 的论文，所以我打印出来并飞往博洛尼亚。我一直在展示这篇论文并且一直在谈论它。我收到了 Harmonic 的 Aristotle 的 API 密钥。许多参与者都在使用他们作为研讨会参与者收到的 API 密钥尝试 Aristotle（Harmonic 赞助了这次活动）。我看到一位数学家说“看看 Aristotle 生成的这个有趣的证明”。这听起来很有希望。我向 Nico 索要了他的论文的 LaTeX 源代码。我准备在论文上尝试 Aristotle。

使用 Aristotle 和 Claude Code 进行形式化

我第一次要求 Aristotle 形式化这篇论文时，我等了几个小时。我得到了一些 Lean 代码，其中一条评论说预算已用完。我要求 Aristotle 继续，然后等了几个小时。我重复这个过程一段时间，直到 Aristotle 不再产生新的 स्टेटमेंट。

然后我开始在 Aristotle 和 Claude Code 之间来回切换。我要求 Claude Code 将冗长的证明分解为引理，陈述缺失的引理，并添加 स्टेटमेंट 以确保完整性。我要求 Aristotle 证明 Claude Code 陈述的猜想。Aristotle 有时会给出 Claude Code 猜想的反例。Aristotle 有时会证明这些猜想。整个过程大约花费了一个半月（我从来没有完全专注于这个项目）。

对于后处理，我大量使用了 Claude Code。这包括删除从未使用的引理，将引理重新组织到新的文件组织中，并使用对论文特定位置的引用来注释 Lean 代码。

接下来是什么

这个项目的内容非常接近 Arklib 中的 FRI 形式化项目。我认为可以调整这个项目中的定义，以便可以将结果合并到 Arklib 中。Arklib 中的约定将优先于该项目期间发明的任何风格。

我们还可以尝试实例化这个形式化，并具体评估正确性误差。

另一个方向是证明 FRI 验证器的实现与论文中的验证器行为相同。我将尝试找出获得端到端结果的方法。

至于 Charlie，他需要学习阅读 Lean 的定义和 स्टेटमेंट，尽管可能不一定需要阅读证明。说实话，他仍然需要了解一些密码学才能看到 Lean 中的结果很重要。但现在，Charlie 不会完全迷失方向。当某些证明步骤似乎缺失时，Lean 形式化中详细的引理可能会有所帮助。

感谢

这个项目是由 Nico 发起的。他还就这篇文章给了我反馈。 由于可以访问 Aristotle，这个形式化项目才有可能实现，Aristotle 有时会产生非常复杂的证明。 ItaLean 2025 非常适合与其他 Lean 和自动形式化代理的用户和创建者互动。 Claude Code（甚至是 Sonnet 4.5）在 Lean 方面出奇地好。我认为我很幸运能在这个历史时刻出现。

此帖子的缩略图由 Nano Banana Pro 生成。

zkSecurity 为包括零知识证明、MPC、FHE 和共识协议在内的密码系统提供审计、研究和开发服务。

了解更多 →

• 原文链接： blog.zksecurity.xyz/post...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～