← 피드로
[Submitted on 25 Sep 2026]
Abstract:AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and bears the full computational cost. We introduce Choir, an open protocol for distributed formalization. Choir decomposes a project into tasks that can be completed by independent contributors, each running their own agent with their own LLM subscription, while coordinating entirely through the project’s GitHub repository. To support open participation, every contribution is checked by a deterministic gate before merge. Choir supports Lean 4, Isabelle, and Rocq, and is open source and modular, allowing projects to replace individual components or extend the protocol.
Submission history
From: Yidi Qi [view email]
[v1]
Fri, 25 Sep 2026 18:44:53 UTC (849 KB)
추출 본문 · 출처: arxiv.org · https://arxiv.org/abs/2609.31903