Harvard выпустила Choir: открытый протокол, где обмен задачами о формализации идёт через GitHub, а каждый pull request проходит детерминированный гейт доверия до ревью
Yidi Qi и Melanie Weber из Гарварда опубликовали Choir, - открытый протокол распределённой автоформализации.
В протоколе реализован обмен задачами через GitHub, - репозиторий превращается в координационный слоем, где план превращается в задачи, задачи - в pull request’ы, а merge возможен только после детерминированного гейта доверия.
🧠 Протокол обмена через GitHub:
- Оркестратор публикует задачи как issues: формулировка готова, доказательство, - placeholder, метки сложности
- Контрибьютор забирает задачу комментарием (кто первый, того аренда), доказывает своим агентом, отдаёт PR из форка
- Если теорема не влезает в один PR, воркер декомпозирует её на леммы, - дерево растёт от тех, кто щупал математику
- Детерминированный гейт на GitHub Actions проверяет PR до ревью: пересборка, запрет аксиом, отсутствие sorry, неизменность формулировки
- Визуализатор реплеит историю: дерево доказательств, кто какую ветку доказал
- Lean 4, Isabelle и Rocq, Apache 2.0, плагины для Claude Code и Codex
💼 Зачем бизнесу:
Архитекура позволяет добиться решения задачи даже если исполнители распределены и вы можете даже в принципе не знать что за воркер выполняет задачу, - merge без прохождения механического гейта невозможен, - ревью оркестратора идёт когда гейт уже провел все предварительные проверки.
GitHub даёт протоколу то, что отдельно пришлось бы долго настраивать, - идентичность, триггеры событий, права, публичный аудит.
Система обмена задачами с механической приёмкой результата годится для любого домена с проверяемым результатом.
#Choir #Lean4 #автоформализация #мультиагентность #агенты
———
@tsingular | Max | YouTube | RuTube | VK | VK Video | Дзен