Choir README

The project's README from github.com/Weber-GeoML/Choir. As one markdown file: README.md.

Choir

An open protocol for distributed multi-agent autoformalization.

CI License: Apache 2.0 Python 3.11+ Status: pre-alpha

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:

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.

Choir (Weber-GeoML/Choir)

Searching Database…

116 ·GitHub
Choir
这是什么？Choir 是一个用于分布式多智能体自动形式化的开放协议：由一名人类监督者运行编排智能体，把一个大型形式化项目拆解成 GitHub 仓库上的任务，其他贡献者认领这些任务并用各自的智能体完成，费用各记各的账户。
这是独立应用，还是接入我已有工具的插件？它以 Claude Code 和 Codex 插件的形式发布，本仓库就是这两种宿主的插件市场；它自身没有任何内置行为，只有任何智能体都能照着执行的安装脚本和 playbook。
它支持哪些编码智能体和证明助手？Choir 开箱即支持 Claude Code 或 Codex，也支持任何能读取其 playbook 并运行 shell 脚本的其他智能体；在证明方面，它支持 Lean 4、Isabelle 和 Rocq。
Choir 会自动检查提交的证明吗，还是审阅全靠人工？每个提交的 pull request 都会先经过 Choir 的确定性信任门检查，然后才由人工审阅并合并，但实际的定理证明工作仍由贡献者自己的智能体完成，而不是 Choir 本身。
CLI 运行在哪些平台上？Choir 是一个通过 shell 脚本驱动的 Python CLI，旨在运行在参与者直接控制的 Linux 和 macOS 机器上。
信任门到底是什么？它是一个确定性的自动检查，在人工审阅或合并决定之前审计每个提交的 pull request 中的证明，尽早过滤掉无效的形式化。
有 Choir 实际使用的真实例子吗？ProbMethodCombinatorics 是一个由 Choir 驱动的项目，对 Yufei Zhao 的《Probabilistic Methods in Combinatorics》讲义进行自动形式化，产出了 285 个用 Lean 4 加 Mathlib 证明的定理。
我可以替换默认的规划器或编排器吗？可以，默认的规划器和编排器被明确设计为可以换成你自己的实现，或嵌入现有的工作流。
What are similar projects?openrig, harness, Agentlas-OS, oh-my-subagents, hyperfide, hive, pstack-claude, open-swe
Which topics is it in?theorem-proving, verification, marketplace, codex-cli, protocol, multi-agent-systems, claude-code-plugin, academic, autonomous-agents, github, workflow-automation, agent-orchestration
Creator
Weber-GeoML
Size
2.1 MB
Stars
116
Updated
CommitOct 18
Age
28d
Commits · 90 Days