Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics (www.renaissancephilanthropy.org)

Renaissance Philanthropy has launched the Mathlib Initiative to professionalize and scale Mathlib—the open-source Lean library that now contains nearly two million lines of computer‑verified mathematics—backed by a donation from Alex Gerko and led by Johan Commelin, Oliver Nash and Adam Topaz. The initiative targets critical bottlenecks: August 2025 saw Mathlib’s busiest month (≈1,100 community contributions reviewed), yet roughly 2,000 pull requests remain unreviewed. Kevin Buzzard and Alex Kontorovich argue that increasing review bandwidth, funding specialist “refactors” to extract reusable lemmas, and smoothing integration between large projects (e.g., FLT and the 30,000-line PNT+ work) and Mathlib will accelerate formal research, reduce friction for contributors, and turn big project outputs into canonical library pieces rather than siloed blueprints. They also stress education and AI synergies: the steep Lean learning curve and shrinking entry-level tasks for students demand curated, pedagogical resources (course material, translated textbooks, “games” for core topics). On AI, both see promise but caution—no AI has yet independently proved a novel theorem, yet autoformalization (translating LaTeX/papers into Lean) could be transformative, enabling AI-assisted refereeing and dramatically lowering the “formalisation coefficient.” Practical obstacles remain—definitions, tooling and review capacity—but the Initiative’s funding and professional roles aim to turn formal verification from a niche volunteer effort into sustainable infrastructure for AI‑era mathematics.