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 даёт протоколу то, что отдельно пришлось бы долго настраивать, - идентичность, триггеры событий, права, публичный аудит.

Система обмена задачами с механической приёмкой результата годится для любого домена с проверяемым результатом.

paper | GitHub

#Choir #Lean4 #автоформализация #мультиагентность #агенты
———
@tsingular | Max | YouTube | RuTube | VK | VK Video | Дзен