Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

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.

Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO); Multiagent Systems (cs.MA)

arXiv:2609.31903 [cs.AI]

(or arXiv:2609.31903v1 [cs.AI] for this version)

https://doi.org/10.48550/arXiv.2609.31903 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.