Abstract
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. We introduce Choir, an open protocol for distributed formalization. Choir decomposes a project into tasks that can be completed by independent contributors, each running their own agent with their own LLM subscription, while coordinating entirely through the project's GitHub repository. To support open participation, every contribution is checked by a deterministic gate before merge. Choir supports Lean 4, Isabelle, and Rocq, and is open source and modular, allowing projects to replace individual components or extend the protocol.
Keywords
Subject
Publication details
- Journal
- Not available
- Open access
- Green open access
Cite this article
APA 7
Qi, Y., & Weber, M. (2026). Choir: An Open Protocol for Distributed Multi-Agent Autoformalization. https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization
MLA 9
Qi, Yidi, and Melanie Weber. "Choir: An Open Protocol for Distributed Multi-Agent Autoformalization." https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization.
Chicago (author–date)
Qi, Yidi, and Melanie Weber. 2026. "Choir: An Open Protocol for Distributed Multi-Agent Autoformalization." https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization.
Harvard
Qi, Y. and Weber, M. (2026) 'Choir: An Open Protocol for Distributed Multi-Agent Autoformalization', Available at: https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization.
Vancouver
Qi Y, Weber M. Choir: An Open Protocol for Distributed Multi-Agent Autoformalization. https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization
IEEE
Y. Qi, and M. Weber, "Choir: An Open Protocol for Distributed Multi-Agent Autoformalization," https://omanscience.com/en/articles/choir-an-open-protocol-for-distributed-multi-agent-autoformalization.