普林斯顿开源 Choir 协议：多智能体协同做大规模数学形式化

普林斯顿团队在 Darpa expMath 项目支持下开源 Choir 协议，用于分布式多智能体自动形式化，把单个数学家的人工证明扩展到大规模自动化。人类监督者在本地运行编排 agent 拆解任务并挂到 GitHub 仓库，贡献者用自己付费的 agent 认领完成，所有提交的 PR 先通过 Choir 的确定性信任门自动审计，再进入人工评审与合并。