Choir：一个用于分布式多智能体自动形式化的开放协议
Choir: An Open Protocol for Distributed Multi-Agent Autoformalization
AI总结：
Choir是一个开放协议，通过GitHub协调独立贡献者运行各自智能体，实现分布式多智能体自动形式化，支持Lean 4、Isabelle和Rocq，并具备确定性门控检查。
AI中文摘要：
AI智能体现在能够在Lean等证明助手中形式化整本教科书和主要定理，但当前的努力通常是集中式的：单个团队运行所有智能体并承担全部计算成本。我们引入了Choir，一个用于分布式形式化的开放协议。Choir将项目分解为可由独立贡献者完成的任务，每个贡献者运行自己的智能体并使用自己的LLM订阅，同时完全通过项目的GitHub仓库进行协调。为了支持开放参与，每个贡献在合并前都经过确定性门控检查。Choir支持Lean 4、Isabelle和Rocq，并且是开源和模块化的，允许项目替换单个组件或扩展协议。
英文摘要：
AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and bears the full computational cost. We introduce Choir, an open protocol for distributed formalization. Choir decomposes a project into tasks that can be completed by independent contributors, each running their own agent with their own LLM subscription, while coordinating entirely through the project's GitHub repository. To support open participation, every contribution is checked by a deterministic gate before merge. Choir supports Lean 4, Isabelle, and Rocq, and is open source and modular, allowing projects to replace individual components or extend the protocol.
