Moving from individual proofs to large-scale autoformalization requires new tools. We introduce Choir, an open protocol for multi-agent autoformalization that decomposes projects into tasks, coordinates contributions through GitHub, and deterministically checks them before merging.

Choir is modular, open source, and supports Lean 4, Isabelle, and Rocq.

Repository: https://github.com/Weber-GeoML/Choir…

Preprint: https://arxiv.org/abs/2609.31903

Led by @yidi_qi. Supported by @darpa expMath.

Weber-GeoML/Choir

Source: https://github.com/Weber-GeoML/Choir

An open protocol for distributed multi-agent autoformalization.

Choir aims to spread the cost of a large formalization. A human overseer runs an orchestrator agent on their own machine; Choir turns that agent’s plan into tasks on a GitHub repo, where any contributor can claim one and work it with their own agent, billed to their own account. Every submitted pull request is audited by Choir’s deterministic trust gate before it is reviewed and merged. Works with Lean 4, Isabelle and Rocq, and with whichever agent each participant already runs. The default planner and orchestrator are easy to swap for your own, or to slot into a workflow you already have.

See a demo repo: ProbMethodCombinatorics is a Choir-powered autoformalization of Yufei Zhao’s Probabilistic Methods in Combinatorics lecture notes — 285 theorems in Lean 4 with Mathlib.

Read the paper: Choir: An Open Protocol for Distributed Multi-Agent Autoformalization.

Getting started

With Claude Code or Codex

Choir ships as a plugin, and this repo is the marketplace for both harnesses.

In a Claude Code session:

/plugin marketplace add Weber-GeoML/Choir
/plugin install choir@choir

In your shell, for Codex:

codex plugin marketplace add Weber-GeoML/Choir
codex plugin add choir@choir

Then say what you want in plain language:

• “Formalize ‹your theorem, paper, or chapter› with Choir”: start or resume a project as its overseer.
• “Join ‹owner/repo› as a Choir contributor”: set this machine up to prove tasks as a worker.

Explicit invocation works too: /choir:formalize and /choir:join owner/repo in Claude Code, $choir:formalize and $choir:join owner/repo in Codex. You can also add your own instructions on top of them.

With any other agent

The plugin defines no behaviour. Its skills only run the setup scripts and defer to the playbooks, so any agent can drive Choir. Both roles work the same way: read a playbook, call the CLI. Paste the relevant prompt:

To run a project (overseer):

Clone https://github.com/Weber-GeoML/Choir to ~/.choir/checkout if it isn’t already there, then read ~/.choir/checkout/docs/agents/ORCHESTRATOR.md and act as the orchestrator for ‹goal, sources, or owner/repo›. Follow that playbook; don’t improvise steps its scripts already own.

To contribute proofs (worker):

Clone https://github.com/Weber-GeoML/Choir to ./choir, run sh ./choir/scripts/join.sh ‹owner/repo› and fix whatever it flags until it reports READY, then read ./choir/docs/agents/CONTRIBUTOR.md and work by it. You do the proving yourself: claim a task, close the placeholder, submit.

The playbooks in docs/agents/ cover both roles in full.

License

Apache-2.0. See LICENSE.