cs.AISep 25, 2026

Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

Authors: Yidi Qi, Melanie Weber

Organizations: Harvard University

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

RoleRuns whereDoes
Overseer— (human)Owns the project. Sets the goal, the audit policy, and how far the orchestrator may act alone, and rules on new axioms.
Orchestratoroverseer’s machine, LLM account, and GitHub authPlans and decomposes the goal, authors the statements , publishes typed tasks, reviews and merges pull requests, replans in a loop.
Workerscontributors’ machines and accountsClaim a task, prove it with the contributor’s own agent, submit. Hold no repository write access: a claim is a comment, a submission is a pull request from the contributor’s own fork.
GateGitHub Actions in the project repoDeterministic audits and intake validation.
Table 1: The four roles.
Figure 1: The orchestrator publishes tasks as GitHub issues, and workers on contributors’ own machines claim them and submit pull requests. The gate audits each pull request before the orchestrator reviews and merges it.
PartyCommandWhat it does
Orchestratorchoir orch pollBlocks until a task or a pull request changes, then exits with a JSON summary of what changed. The loop’s clock.
 choir orch create-taskPublishes a task issue from a plan node
 choir orch prsOpen pull requests, with the verification gate’s results
 choir orch merge ∣\mid closeMerges a pull request, or closes it unmerged. merge refuses unless the gate passes.
 choir orch commentPosts a comment on a task issue or a pull request
 choir orch sync-leasesReads the comments from workers and updates task labels
Table 2: Choir’s most-used commands.
Figure 2: The path of a pull request. The gate’s checks run first, and only a pull request that passes them reaches the orchestrator’s review. When either stage rejects it, the orchestrator can republish the task, from scratch if the work is unsound or from the partial work if it is a near miss.
Figure 3: Part of the Zhao formalization’s proof tree in the history visualizer, partway through the project. Blue fill marks proved nodes, a blue outline published tasks, and each other color one worker’s claim; rounded boxes are definitions.
More in this topic

Multi-Agent Collaboration

Multi-agent collaboration studies how autonomous agents coordinate, share information, and combine capabilities to solve tasks together.

See all 309 papers

Explore similar work

CardsList

  1. Prove2Me: An Open Collaborative Platform for Scaling Math Formalization

    Aug 28, 2026Shuze Chen, Kunal Marwaha, Xiaoyang Lu +2Multi-Agent CollaborationLean Theorem Proving

    Graduate School of Business Columbia University New York, NY 10027 · Department of Computer Science University of Chicago Chicago, IL 60637 · Department of Computer Science Purdue University West Lafayette, IN 47907 +1

  2. LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

    Jun 3, 2026Yuanhe Zhang, Yuekai Sun, Taiji Suzuki +2Lean Theorem ProvingAutoformalization

    Department of Statistics, University of Warwick, UK · Center for Advanced Intelligence Project, RIKEN, Japan · Department of Statistics, University of Michigan, USA +3

  3. Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

    Mar 6, 2026Chad E. Brown, Cezary Kaliszyk, Josef UrbanAutoformalizationMulti-Agent Collaboration

    AI4REASON · University of Melbourne · AI4REASON, University of Gothenburg and Chalmers University of Technology