Choir：用于分布式多智能体自动形式化的开放协议

研究人员推出开源协议 Choir，用于实现分布式多智能体定理自动形式化。Choir 将形式化项目分解为独立任务，支持各贡献者运行自带 LLM 订阅的 AI 智能体并通过 GitHub 协作，所有提交均由确定性门控检查后合并。该协议采用模块化设计且支持扩展，目前已兼容 Lean 4、Isabelle 和 Rocq。