# Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

arXiv: https://arxiv.org/abs/2609.31903 · HTML: https://mlsanity.com/paper/2609.31903/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 15 of its 29 references that are in the map.
- First posted on arXiv 25 Sep 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 15 of 15)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale](https://mlsanity.com/paper/2512.07087/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [Prove2Me: An Open Collaborative Platform for Scaling Math Formalization](https://mlsanity.com/paper/2608.28433/) (2026)
- [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026)
- [Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents](https://mlsanity.com/paper/2603.06737/) (2026)
- [Multi-agent Autoformalization of Tensor Network Theory](https://mlsanity.com/paper/2607.07857/) (2026)
- [Long-horizon autoformalization of a core theorem underlying MIP* = RE](https://mlsanity.com/paper/2609.19814/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)

## Abstract (arXiv)

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.