The paper introduces Choir, an open protocol designed to distribute large autoformalization projects among independent contributors. It responds to the centralized structure of current efforts, in which one team operates all agents and pays the full computational cost. Choir breaks a project into tasks that contributors can complete separately using their own agents and LLM subscriptions. Coordination takes place through the project’s GitHub repository rather than a centrally managed agent operation. Before a contribution is merged, a deterministic gate checks it, providing a consistent requirement for open participation. The protocol supports Lean 4, Isabelle, and Rocq proof assistants. It is open source and modular, so projects can replace individual components or extend the protocol. The paper was submitted to arXiv on September 25, 2026.
