Choir：通过GitHub协调分布式多Agent形式化证明

AI Agent现在能够在Lean等证明助手中形式化整本教材和重大定理，但现有工作通常是集中式的：一个团队运行全部Agent，承担所有计算成本。我们提出Choir，一个分布式形式化的开放协议。Choir把项目拆成独立贡献者可完成的任务；每位贡献者使用自己的LLM订阅运行自己的Agent，协调完全通过项目GitHub仓库完成。为支持开放参与，每项贡献都在合并前通过确定性门禁检查。Choir支持Lean 4、Isabelle和Rocq，具有开源、模块化特点，允许项目替换单个组件或扩展协议。