Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

• Recent large-scale agent formalizations have typically relied on one team running all agents and bearing the computational cost.One effort used about 30,000 agent runs and was estimated to cost $100K with prompt caching or $430K without [8].Source: §1 · p. 1
• Choir lets independent contributors formalize project tasks using their own agents and LLM subscriptions, coordinating through GitHub.It supports Lean 4, Isabelle, and Rocq and is open source and modular.Source: §1 · p. 2
• Choir’s task system distributes formalization across contributors’ agents and lets the proof tree grow through returned decompositions.The orchestrator can publish tasks for child results and repeat the decomposition loop.Source: §1 · p. 2
• A deterministic gate re-checks each pull request mechanically before the orchestrator reviews it.The gate checks that the published statement is unchanged.Source: §1 · p. 2
• A history visualizer replays proof-tree growth and identifies who proved or decomposed each node from GitHub records.Source: §1 · p. 2
• Choir was tested by formalizing Yufei Zhao’s Probabilistic Methods in Combinatorics in Lean 4, a textbook also included in Meta FAIR’s Atlas.Its inclusion in Atlas makes a direct comparison possible.Source: §1 · p. 2

Plan

• The orchestrator records a roadmap and dependency graph, publishes only nodes whose statements and dependencies are formalized, and deliberately leaves deeper decomposition to workers.Planners can be replaced with custom planners or human-written files if the roadmap format is preserved.Source: §2 · p. 3

Publish

• The orchestrator publishes ready nodes as GitHub issues with placeholder proofs, difficulty, and priority; overseers can cap task difficulty for particular workers.Source: §2 · p. 3

Prove and submit

• Contributors prove tasks on their own machines using any agent or workflow that follows Choir’s task and submission rules, then submit pull requests through GitHub.GitHub handles coordination and version control through commands implemented as wrappers over its CLI.Source: §2 · pp. 2, 4

Decompose

• Workers can decompose a difficult task into intermediate lemmas, and accepted decompositions let the orchestrator update dependencies and publish child tasks, extending the proof tree.Child tasks can enter the same decomposition loop.Source: §2 · p. 4

Review and merge

• The gate checks each pull request before the orchestrator reviews mathematical soundness and decomposition quality; both stages must pass before merge, and rejected work may be republished with or without partial results.Source: §2 · p. 5, Figure 2 · p. 5

Golf

• A golf task asks workers to shorten an already-proved declaration without changing its statement, either by returning a shorter proof or factoring it with auxiliary lemmas.Source: §2 · p. 5

• Every pull request is checked automatically from source under merge-base policies, and the merge command refuses it unless all required checks are present and every blocking check is green.Source: §3 · p. 5
• The gate checks fresh-checkout compilation, rejects new axioms, and blocks unresolved proof placeholders unless the worker declares a decomposition for orchestrator review.Source: §3 · pp. 5–6
• Lean 4 statement immutability can be checked through the Lean FRO comparator, which follows the statement through its dependencies down to definition bodies.Source: §3 · p. 6
• Isabelle and Rocq lack an equivalent immutability tool, so source-text checks can miss changed meanings or smuggled assumptions, leaving detection to orchestrator and human review.A contradictory hypothesis in scope can permit proofs of false statements by explosion.Source: §3 · p. 6

• The timeline is derived from the repository’s git log, issues, and pull requests and written as a single HTML page.Source: §4 · p. 6
• The visualizer replays dated project events and colors proof-tree nodes by status while giving each worker claim its own hue, showing where proofs and decompositions came from.Users can step through events with a slider or play button.Source: §4 · p. 6
• The page lets human overseers follow project progress.Source: §4 · p. 7

• Unlike systems where one team runs every agent on its own compute and budget, Choir’s workers are other people’s agents running on their own machines and accounts.Source: §5 · p. 7
• Choir combines roadmap-driven GitHub pull requests and fixed statements with a deterministic gate, and differs from related platforms as infrastructure any project can set up on its own repository.TauCeti also distributes roadmap work through GitHub pull requests, while Prove2Me fixes statements before proofs are submitted.Source: §5 · p. 7

6 Limitations and next steps

• The architecture has not been tested beyond textbook scale, and a hierarchy of orchestrators is only a proposed fallback.The design uses shallow skeletons and groups related results so the orchestrator can focus on the relevant part of a project.Source: §6 · p. 7
• For Isabelle and Rocq, a statement can change meaning without changing its source text, leaving detection to review rather than the mechanical check.The authors plan to close this gap mechanically in a future version.Source: §6 · p. 7
• Choir has mainly been tested on textbook-level Lean 4 autoformalization, while larger-scale runs with open-source models and harnesses are invited.The authors expect large-scale formalization to become feasible for academic groups and hobbyists working with subscriptions and open-source models.Source: §6 · pp. 7–8