Formal Frontier

Scope

The initial phase of the project has three main components.

First, we will develop and release an autoformalization specification in coordination with the community and other stakeholders. This specification will articulate community standards for metadata that should accompany autoformalized artifacts. It will cover questions such as:

• How the formal code relates to the informal source.

• What counts as adequate coverage and faithfulness.

• How the artifact relates to the Mathlib ecosystem.

It will also address the broader lifecycle of autoformalized artifacts, including:

• Human oversight and maintenance.

• Licensing.

• Coordination with related projects.

• Upstreaming plans.

We expect this specification to serve as a shared reference point for autoformalization projects and the formal mathematics community. By adopting it, projects can give the community a clearer basis for evaluating, trusting, and building on autoformalized work. Work on the specification is already underway, and we will make a follow-up announcement in the next couple of weeks.

Second, we will release open-source autoformalization tooling. Autoformalization work is inevitably constrained by model access, inference costs, and mathematical expertise, but tooling such as harnesses, orchestration systems, and dashboards should be widely available as open source. Access to basic tooling should not be a limiting factor.

Finally, Formal Frontier will produce and release autoformalized mathematical artifacts that embody the standards this project promotes. We will autoformalize mathematical texts chosen to fill gaps in Mathlib's existing coverage, focusing particularly on prerequisites for serious formalization work in research-level mathematics. Our main priority is to provide the community with high-quality, scalable code that can be built on by both human and AI formalizers.

Why Now?

At the Mathlib Initiative, we view Lean and Mathlib as part of the mathematical infrastructure of the future. For this future to become a reality, the scalability of Mathlib and its ecosystem must remain a top priority. This is why much of our work has focused on review capacity, downstream coordination, documentation, and other key infrastructure. Formal Frontier is the next step in that same direction.

Mathlib already contains about 2 million lines of formally verified mathematics, written by over 750 contributors. When a definition or theorem becomes part of Mathlib, it becomes part of this mathematical infrastructure. It must therefore be written in a way that is maintainable and scalable.

In recent months, autoformalization has moved from an occasional demo to something that will clearly play a central role in the future of formalized mathematics. This has made the issue of scalability much more urgent.

As autoformalization systems improve, we should expect a flood of Lean code that typechecks. The central question will not be whether the kernel accepts more generated proofs, but whether those artifacts can become useful mathematical infrastructure. We believe that scalability, not lines of code or the number of formally verified theorems, is the metric by which autoformalized artifacts should be judged. Scalability is a global property of the ecosystem, not of any particular definition or theorem.

Verified output can still duplicate existing material, introduce bad definitions, ignore established APIs, or leave behind brittle and unmaintainable proofs. The number of formally verified theorems may increase, but so does the burden on those who maintain the library and those who use the results. Such output hinders the scalability of the ecosystem as a whole. Without intervention, a massive influx of formally verified slop could seriously harm Mathlib, the ecosystem around it, and the role of formal mathematics as shared mathematical infrastructure.

Formal Frontier is that intervention.

Alex Gerko, Founder and CEO of XTX Markets, said, "XTX Markets is pleased to support Formal Frontier and the mathematical community's wider efforts to develop open science. The future of mathematical discovery shouldn't be hidden in a black box or behind a paywall."

Get Involved

Formal Frontier is built with the community in mind, and there are several ways to get involved. If you lead an autoformalization project, reach out about adopting the specification in your work. We want the specification to reflect real work, and early collaborators will help shape it.

If you're a researcher, tell us where Mathlib's gaps are slowing you down. Suggestions for prerequisite material that would unlock serious formalization in your area are especially welcome.

For either of these, or any other questions about Formal Frontier, get in touch through our contact page.