@mweber_PU：从单篇证明走向大规模自动形式化，需要新的工具。我们推出 Choir，一个开放协议……

X AI KOLs Timeline 论文
autoformalization multi-agent lean-4 formal-verification open-source protocol proof-assistant

摘要

作者们提出 Choir——一个用于分布式多智能体自动形式化的开放、模块化协议，将项目拆解为基于 GitHub 的任务，并通过确定性的信任门验证机制进行审核，支持 Lean 4、Isabelle 和 Rocq；该项目包含一篇预印本以及一个由 DARPA expMath 项目资助的开源代码仓库。

从单篇证明走向大规模自动形式化，需要新的工具。我们推出 Choir——一个用于多智能体自动形式化的开放协议，它将项目拆解为任务，通过 GitHub 协调各方贡献，并在合并前进行确定性验证。 Choir 采用模块化设计，完全开源，支持 Lean 4、Isabelle 和 Rocq。 代码仓库：https://github.com/Weber-GeoML/Choir… 预印本：https://arxiv.org/abs/2609.31903 由 @yidi_qi 领导。获 @darpa expMath 资助。
查看原文
查看缓存全文

缓存时间: 2026/10/03 04:50

OpenFormal Protocol

一个用于分布式多智能体自动形式化的开放协议。

该协议为多个自主智能体在分布式环境中协同完成形式化（autoformalization）任务而设计，定义了智能体之间的任务分配、形式化结果表示、验证流程以及通信与协作的标准化接口，从而支持可扩展、可互操作的自动形式化工作流。

相似文章

我们现在有了证明自动化

Hacker News Top

本文讨论了LLMs如何自动生成证明，在如Lean和Rocq这样的依赖类型语言中，通过利用证明无关性并减少手动证明工程的需求，使得形式验证变得更加实用。

评估Lean 4中证明自动形式化的鲁棒性

arXiv cs.CL

本文评估了在全局和局部扰动下，Lean 4中证明自动形式化模型的鲁棒性，发现当前基于LLM的模型对扰动敏感，且常常无法忠实地反映局部变化。

未完成项并非难点：半自动形式化的专家评审案例研究

arXiv cs.AI

本文介绍了一项案例研究，使用大型语言模型（Claude Code）在Lean定理证明器中形式化格罗滕迪克消失定理。研究发现，虽然智能体可以生成经验证的代码，但在定义和API设计方面存在困难，强调了超越单纯编译的专家评审需求。