What is this?
Choir is an open protocol for distributed multi-agent autoformalization: a human overseer runs an orchestrator agent that breaks a large formalization project into tasks on a GitHub repo, which other contributors claim and work with their own agents, each billed to their own account.
Choir is an open protocol for distributed multi-agent autoformalization: a human overseer runs an orchestrator agent that breaks a large formalization project into tasks on a GitHub repo, which other contributors claim and work with their own agents, each billed to their own account.Is this a standalone app, or a plugin for something I already use?It ships as a plugin for Claude Code and Codex, and this repo is the plugin marketplace for both harnesses; it has no built-in behaviour of its own, just setup scripts and playbooks that any agent can follow.
It ships as a plugin for Claude Code and Codex, and this repo is the plugin marketplace for both harnesses; it has no built-in behaviour of its own, just setup scripts and playbooks that any agent can follow.Which coding agents and proof assistants does it support?Choir works with Claude Code or Codex out of the box, and with any other agent that can read its playbooks and run shell scripts; on the proof side it supports Lean 4, Isabelle, and Rocq.
Choir works with Claude Code or Codex out of the box, and with any other agent that can read its playbooks and run shell scripts; on the proof side it supports Lean 4, Isabelle, and Rocq.Does Choir check submitted proofs automatically, or is the review all manual?Every submitted pull request is first run through Choir's deterministic trust gate before a human reviews and merges it, but the actual theorem-proving work is still done by the contributor's own agent, not by Choir itself.
Every submitted pull request is first run through Choir's deterministic trust gate before a human reviews and merges it, but the actual theorem-proving work is still done by the contributor's own agent, not by Choir itself.What platforms does the CLI run on?Choir is a Python CLI driven via shell scripts, intended to run on Linux and macOS machines that participants control directly.
Choir is a Python CLI driven via shell scripts, intended to run on Linux and macOS machines that participants control directly.What is the trust gate exactly?It is a deterministic automated check that audits every submitted pull request's proof before a human reviewer or merge decision, filtering out invalid formalizations early.
It is a deterministic automated check that audits every submitted pull request's proof before a human reviewer or merge decision, filtering out invalid formalizations early.Is there a real example of Choir in use?ProbMethodCombinatorics is a Choir-powered autoformalization of Yufei Zhao's 'Probabilistic Methods in Combinatorics' lecture notes, producing 285 theorems proved in Lean 4 with Mathlib.
ProbMethodCombinatorics is a Choir-powered autoformalization of Yufei Zhao's 'Probabilistic Methods in Combinatorics' lecture notes, producing 285 theorems proved in Lean 4 with Mathlib.Can I replace the default planner or orchestrator?Yes, the default planner and orchestrator are explicitly designed to be swapped out for your own implementation or slotted into an existing workflow.
Yes, the default planner and orchestrator are explicitly designed to be swapped out for your own implementation or slotted into an existing workflow.What are similar projects?openrig, harness, Agentlas-OS, oh-my-subagents, hive, pstack-claude, codify, open-swe
openrig, harness, Agentlas-OS, oh-my-subagents, hive, pstack-claude, codify, open-sweWhich topics is it in?theorem-proving, verification, marketplace, codex-cli, protocol, multi-agent-systems, claude-code-plugin, academic, autonomous-agents, github, workflow-automation, orchestration
theorem-proving, verification, marketplace, codex-cli, protocol, multi-agent-systems, claude-code-plugin, academic, autonomous-agents, github, workflow-automation, orchestration