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, а этот репозиторий — маркетплейс плагинов для обоих харнесов; собственного встроенного поведения у него нет, только скрипты установки и плейбуки, которым может следовать любой агент.
Какие кодинг-агенты и ассистенты доказательств он поддерживает?Choir работает с Claude Code или Codex из коробки и с любым другим агентом, который умеет читать его плейбуки и выполнять шелл-скрипты; на стороне доказательств поддерживаются Lean 4, Isabelle и Rocq.
Choir проверяет присланные доказательства автоматически или всё ревью делается вручную?Каждый присланный pull request сначала проходит детерминированный фильтр доверия Choir, прежде чем человек его отревьюит и сольёт, но сама работа по доказательству теорем всё равно выполняется агентом контрибьютора, а не Choir.
На каких платформах работает CLI?Choir — это Python CLI, управляемый через шелл-скрипты и рассчитанный на машины под Linux и macOS, которые участники контролируют напрямую.
Что именно такое фильтр доверия?Это детерминированная автоматическая проверка, которая аудитирует доказательство в каждом присланном pull request до ревью человеком или решения о слиянии, отсеивая неверные формализации на раннем этапе.
Есть ли реальный пример использования Choir?ProbMethodCombinatorics — автоформализация лекций Yufei Zhao «Probabilistic Methods in Combinatorics» на базе Choir, давшая 285 теорем, доказанных в Lean 4 с Mathlib.
Можно ли заменить стандартный планировщик или оркестратор?Да, стандартные планировщик и оркестратор специально спроектированы так, чтобы их можно было заменить собственной реализацией или встроить в существующий workflow.
What are similar projects?openrig, harness, Agentlas-OS, oh-my-subagents, hive, pstack-claude, codify, 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, orchestration
Creator
Weber-GeoML
Size
2.1 MB
Stars
116
Updated
CommitOct 01
Age
27d
Commits · 90 Days