Choir: An Open Protocol for Distributed Multi-Agent Autoformalization.

arXiv:2609.31903v1 Announce Type: new 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