Roadmap

Current State

Mathlib has over 2 million lines of formally verified mathematics, written by over 750 contributors.

Long-term Goals

The Initiative supports Mathlib's growth toward:

• A comprehensive library of formal mathematics across all levels

• A thriving ecosystem of large-scale collaborative mathematical projects

• Enhanced documentation and educational resources lowering barriers to entry

• AI integration supporting automated reasoning and mathematical research

The Initiative operates within the existing Mathlib community structure, working with current maintainers, reviewers, and contributors to address scaling challenges.

D0. Community Support

Description. Over the past decade, Mathlib's maintainer, reviewer, and moderator structures grew organically through a period of rapid expansion. They have carried the library remarkably far, but they were not designed for the scale the community is now reaching. We support the community's own governance conversation (rather than directing it). Our Community Coordinator supports this process, aiming to listen to the diverse viewpoints and making sure they are considered in the process. We also support mathlib's maintainer team in its day-to-day action: the Community Coordinator facilitates regular maintainer meetings with prepared agendas and circulated notes, and surfaces discussions across Zulip to the people who need to see them. Separately, we are convening the community around Mathlib's tenth anniversary in summer 2027, a moment to celebrate an extraordinary first decade and to set out how much further the second one can go.

Q4 2026

• Mathlib10Conf planning underway: venue, format, and funding scoped

• Regular maintainer meetings continued, with meeting notes published

• Supporting ongoing governance discussions

Q1 2027

• Mathlib10Conf announced: dates, venue, and call for registration published

• Structured maintainer meetings continue running on a regular cadence

• Supporting ongoing governance discussions (as needed)

D1. Rapid Pull Request Triage and Review

Description. Review capacity remains the principal constraint on how fast Mathlib can grow. Over the past year we built the measurement to see this clearly: review-cycle statistics, and daily records of PRs opened against PRs merged. That measurement showed both that our review throughput increased over the year and that the open-PR queue nevertheless continued to grow.

Strategy. We approach the review bottleneck from three angles. First, we sustain and grow the Initiative's own review capacity, which supplies a reliable baseline of roughly 130 review rounds per week. Second, we widen the pool of people able to review, through supporting training events. Third, we reduce the human effort each review requires, by converting recurring review feedback into automated checks and by improving the tools reviewers work with. This may possibly include AI-assisted review for contributors and reviewers that opt-in to such tooling. We will report our statistics publicly.

Our Year 1 target was a response time under one week for 90% of review rounds. This was not achieved (see also our reflection on the first year).

Q4 2026

• Continue to provide significant review resources to Mathlib

• Implement linters and deterministic checks derived from review data, deployed in CI

• Review tooling improved: revamped connected-PRs graph, Lean-aware diffing that reports changed types and values rather than declaration names alone

• Review checklist system defined, with automatable items identified

Q1 2027

• Continue to provide significant review resources to Mathlib

• Effect of the period's interventions on queue health measured and published

• Additional linters and deterministic checks derived from recurring review feedback

D2. Coordinate Ecosystem Infrastructure

Description. The Lean ecosystem downstream of Mathlib is growing rapidly in size while drawing far more public attention. The character of that ecosystem is also changing. Where downstream projects were until recently written by hand, much of the coming growth will be repositories produced with substantial AI assistance. At the same time, the community's users have differentiated: some intend to upstream their work, while many now consume Mathlib without contributing to it. This creates new challenges both in providing services to the community (the olean cache and build runners in particular) and in keeping a much larger ecosystem healthy.

Strategy. We will migrate community infrastructure to an architecture that scales with this growth, and consolidate services that are currently spread across platforms and institutions. We will instrument these services so that we understand how they are used, and use that data to inform and propose sustainable policies with the community (particularly regarding olean caching). We will continue to build tooling that helps downstream projects stay current with Mathlib, upstream their work, and find and reuse work done elsewhere in the ecosystem.

Q4 2026

• Build runners migrated from Hoskinson to Hetzner

• Cache infrastructure migrated to a scalable platform, with a documented transition path for projects holding hard-coded cache URLs

• Cache usage statistics and analysis available; findings reported to the maintainer team

• Queueboard and bors migrated off Heroku

• Queueboard latency reduced

Q1 2027

• Cache usage policy published, following analysis and consultation with heavy users

• Infrastructure for automated repair of downstream breakage in operation

• Upstreaming automation and support tooling available to downstream projects

D3. Documentation

Description. Every tactic defined in Mathlib now carries documentation conforming to the style guide we wrote with the Lean FRO. The tactics that remain undocumented to that standard (roughly 76 relevant to Mathlib users) are defined upstream in Lean core. Beyond reference documentation, the harder problem is findability: the community's accumulated knowledge is substantially held in Zulip threads and in the heads of experts.

Q4 2026

• Verso migration advanced

• Style-guide-conformant documentation extended to tactics in Lean core

• Phrasebook actively promoted within the community, with contribution growing

Q1 2027

• Phrasebook at 50 entries

• Phrasebook findability improved: entries linked from and to module documentation

• A large fraction of Mathlib docstrings use Verso

D4. AI Integration

Description. AI tools have significantly lowered the cost of producing Lean formalizations. The Lean kernel checks that proofs type-check; but it can not check a formalization's semantic alignment with the intended mathematics or its suitability for reuse. We need protocols and tools for provenance, trust, and reuse that make AI-assisted work a useful part of the formal mathematics ecosystem, rather than a collection of disjoint projects with substantial duplication.

Strategy. D4 consists of two complementary projects. Formal Frontier, funded by XTX Markets, develops responsible and reusable autoformalization by producing formalized texts, shared standards, and open-source tooling. Formal Commons, pending funding (expected), develops the protocols and tools needed for a federated ecosystem of independently governed Lean projects, with provenance and trust integral to sharing and reuse.

Q4 2026

• Formal Frontier Phase 1 completed by the end of December 2026

• Autoformalizations of 20 textbooks completed and released

• Formal Frontier standards and tools improved and maintained (formalization.yaml, aftk, tend)

• Model for publishing texts alongside Lean companions developed, with discussions toward initial publisher partnerships underway

• Formal Frontier Phase 2 scoped

Q1 2027

• Formal Frontier Phase 1 assessment published

• Agreement reached with at least one publisher to pilot publication of a text alongside a Lean companion

• Draft Formal Commons protocols for content addressing, portable specifications, and trust claims published for community feedback

• End-to-end prototype demonstrating publication and reuse of a content-addressed Lean artifact across independent projects

Notes. Formal Frontier work beyond Q4 2026 is conditional on additional funding. Formal Commons work depends on completion of its funding contract.

D5. Computations and Metaprogramming

Description. Mathlib excels at proving theorems, but its potential as a platform for verified computation is comparatively underdeveloped. Funded by the Alfred P. Sloan Foundation, this deliverable expands Mathlib in the direction of verified computation and integration with computer algebra systems, together with the metaprogramming infrastructure upon which such work depends. In addition we maintain the metaprogramming infrastructure this work depends on, including quote4, and continue to run the Meta Café, our recurring community session on Lean metaprogramming.

Q4 2026

• Interval arithmetic tactic supporting field operations

• At least one interval arithmetic transcendental function, likely exponential and trigonometric

• Characteristic polynomial tactic

• Computationally efficient representation of matrices

• Computationally efficient dense representation of univariate polynomials

Q1 2027

• At least one root isolation tactic for univariate polynomials

• Primality testing tactic, potentially certificate-based following Lau–Mehta PrimeCert

• Univariate polynomial irreducibility tactic

• Computationally efficient representations of univariate and multivariate polynomials, both sparse and dense

• Computationally efficient representation of finite fields

Implementation

This roadmap will be implemented by our dedicated team working in close coordination with the Mathlib community. To support this work and help accelerate the future of formal mathematics, learn about funding opportunities and partnerships.