---
id: 20260930-T0-10
title: "Choir：分布式多智能体自动形式化的开放协议"
title_en: "Choir: An Open Protocol for Distributed Multi-Agent Autoformalization"
url: https://ai.daily.yangsir.net/daily/20260930-T0-10
issue_date: 2026-09-30
publish_date: 2026-09-29T04:00:00.000Z
category: research
source_name: "arXiv cs.AI"
source_url: https://arxiv.org/abs/2609.31903
---

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

AI 智能体已经能在 Lean 等证明助手中形式化整本教科书和重要定理，但现有工作通常是中心化的：由单一团队运行所有智能体并承担全部算力成本。Choir 提出一套开放协议，把形式化任务分散到多个参与方，共同完成多智能体自动形式化。该协议旨在降低单个团队的计算负担，让更多研究者和机构能参与定理形式化。对数学与形式化验证社区而言，这意味着可以像分布式计算一样协作处理大规模形式化任务，而不必依赖单一机构集中投入资源。

## English Version

**Choir: An Open Protocol for Distributed Multi-Agent Autoformalization**

AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and bears the full computational cost. Choir introduces an open protocol that distributes formalization work across multiple participants to jointly perform multi-agent autoformalization. The protocol aims to reduce the compute burden on any single team and let more researchers and institutions take part in theorem formalization. For the math and formal verification community, this means handling large-scale formalization collaboratively, like distributed computing, rather than relying on one organization's concentrated resources.

---

**来源**：[arXiv cs.AI](https://arxiv.org/abs/2609.31903)

**详情页**：https://ai.daily.yangsir.net/daily/20260930-T0-10

---

*智语观潮 · Daily — https://ai.daily.yangsir.net/llms.txt*