Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

Yidi Qi, Melanie Weber

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 b…