Choir 分布式形式化协议

当前用 Lean 等证明助手形式化教科书与定理的工作多为集中式，由单一团队承担全部算力成本。Choir 提出开放协议，将项目拆解为可由独立贡献者完成的任务，各自运行自己的智能体与 LLM 订阅，通过 GitHub 仓库协调，合并前经确定性门禁校验。协议支持 Lean 4、Isabelle 与 Rocq，开源且模块化。

论文提出 CHOIR 框架，将认知人类学的自由列举方法迁移到大模型集成，通过反复获取排序列表、聚类为提示级概念并测量跨模型、提示变体与人格条件下的概念显著性。在 Infinity-Chat 100 与 27 题诊断集上，表面一致性很高（93/100 高于随机），但基础模型身份仍是最强可恢复特征，人格提示只在基础模型签名内移动概念。