Choir moves autoformalization from one centrally run agent fleet to a GitHub-coordinated protocol where independent contributors run their own LLM agents and pay their own compute. For teams shipping formalization pipelines, the key shift is cost and throughput distribution: you can scale Lean 4, Isabelle, or Rocq projects through external agent contributors, but your merge safety depends on a deterministic verification gate rather than trusting contributor infrastructure.