Choir 提出分布式多智能体自动形式化开放协议，把大型 formalization 拆成可由不同贡献者独立完成的任务

Choir 将大型形式化项目拆成可独立领取的任务，贡献者可用各自的 LLM subscription 和本地 agent 完成子任务，并通过 GitHub 仓库协调。每项贡献在合并前经过 deterministic gate；协议支持 Lean 4、Isabelle 与 Rocq。作者还给出一个 Choir 驱动的教材形式化示例：Yufei Zhao《Probabilistic Methods in Combinatorics》讲义中的 285 个 Lean 4 定理。