A group of mathematicians and formalization researchers argues that AI can help formalize most of mathematics within three years, but only if the resulting Lean libraries are reusable, reviewed, documented, and governed by mathematical communities. They warn that rapidly generated code has limited value when nobody can understand, extend, or trust it. The authors cite an AI-generated formalization of Maryna Viazovska’s sphere-packing work that its original team discarded because cleanup was harder than rebuilding it, and say Anthropic’s 13-million-line, 11-day formal verification of Fermat’s Last Theorem is unlikely to replace a more modern formalization. They support coordinated efforts built around Mathlib, an open-source Lean library with 65 reviewers and 950 contributors that received the 2026 Jean-Pierre Demailly Prize for Open Science in Mathematics. Tau Ceti uses AI-written contributions and AI adversarial review under expert-curated roadmaps; it has grown beyond Mathlib’s 3 million lines of code and includes results such as Riemann–Roch and Chebotarev density. Formal Frontier uses AI-agent systems to turn source texts into interconnected libraries, with 41 released libraries totaling about 200,000 lines. The authors call for open-source interoperability, public review, avoidance of duplicated results, links to literature, sustained compatibility with Lean and Mathlib, and mathematician control over infrastructure and resources.