The Lean FRO Year 4 - Part 1 Roadmap

UX: Workbench, Verso, and Verso Blueprints🔗

Our next-generation UX work shifts from prototyping to maturity and adoption. The core pieces exist today: Verso produces PDFs and interactive web pages from a single literate source, Verso Blueprints brings dependency-graph project views into the same framework, and the Workbench, our zero-install web environment, is in beta testing with external users. The deliverable for this period is turning these prototypes into tools people rely on for real work: hardening Verso, Blueprints, and Games for reliability, performance, and everyday usability, unified by the Workbench interface, and smoothing onboarding for the mathematicians and educators already building on them.

Success is measured in two ways: active users, and published evidence. By the end of the period we expect high-quality documents, papers, and educational material authored with these tools and published in the wild. This exercises the full literate stack and gives the community a substantial, openly available resource built entirely in our system.

Trust🔗

External checking must become a routine part of every Lean user’s workflow, not an expert-only activity. We will ship new Lake commands that make this trivial: lake check exports a development and rechecks it with the official kernel, including the comparator prelude checks; lake check <kernel> does the same with an alternative checker such as nanoda; and lake check --paranoid rechecks with all kernels shipped with Lean, including the new independently developed kernels. We will include comparator in the Lean distribution.

We will also add a mode where lake build skips the official kernel checks and only produces oleans. Users then run lake check to validate everything with their favorite checker. This separation helps users understand what lake build does and does not guarantee, and makes independent checking the default habit.

We will also continue the actions described in our postmortem for issue #14576: adding checks that harden kernel invariants, collaborating with AI research teams that have access to next-generation models, and supporting the development of new external kernels.

Scalability: Mathlib and software verification🔗

We will continue working on scalability, both for Mathlib and for software verification. On the performance side, we will deliver significant improvements to typeclass inference and other elaboration components through granular caching. The typeclass instance caching prototype already shows significant gains on all of Mathlib; this period we turn prototypes into merged, maintained infrastructure.

On the software verification side, we will complete the new do notation, including first-class support for intrinsic verification, and deliver improvements to the verification-condition generator along with further foundational verification tooling. These are the building blocks that let external teams verify real software in Lean. We will also continue improving the performance of SymM, our new tactic framework, which is used to implement the verification-condition generator, Velvet, and, in the future, Aeneas.

Proof automation🔗

We will continue investing in grind and bv_decide. The focus is robustness, integration, and new features requested by the Lean community. We are adding the option to use bv_decide and grind together, and we will focus on quick failure: when the automation cannot close a goal, it should fail fast and tell the user why, instead of consuming time and resources. We will also expand the grind => and sym => interactive modes.

We will improve the documentation for these tactics, and ensure AI agents can use them effectively. AI-generated proofs are becoming a major source of grind and bv_decide usage, and the tactics, their error messages, and their documentation must work as well for agents as they do for humans.

Standard library completion🔗

Standard library development continues on two fronts. First, we will eliminate long-standing issues in fundamental parts of the library and basic data types, and move these modules close to stabilization. Second, we will keep innovating rapidly in the advanced parts of the library: adding missing components, improving usability guided by real use cases, and providing improved alternative APIs for the legacy I/O modules.

Alongside this, we will introduce infrastructure to ensure the quality of material nearing stabilization: additional linters, quantitative quality metrics to observe library quality over time, and manual tracking of global consistency properties using our QA tool Grove.

Tooling🔗

We will ship the code formatter and refine it continuously in communication with the community. We will deliver a simple FFI from Python, followed by further languages. The foundation is Nerodia, our Lean/Python FFI inspired by PyO3: Python modules written entirely in Lean and built with Lake, with type conversions and bindings generated automatically. Nerodia is public but still has a limited API; in this period we will expand its coverage and make it the supported path for calling Lean from Python. Python is the priority: the AI ecosystem is dominated by Python, and it is unrealistic to expect those users to switch languages. We will also continue our work on downstream regression testing (behavioral and performance-wise), usable both by the core libraries and by Lean projects.

lean-beam is how AI agents interact with Lean, and it is strategically important: customers have told us directly that agent tooling should ship with Lean and be available everywhere. Today it is available as a preview but in this period, we will turn it into a product: stabilize it, resolve the architecture questions around combining it with disk-based elaboration resumption, distribute it with Lean, and use it ourselves daily.

AI projects🔗

We run three AI projects at the FRO. Tau Ceti is AI-authored Lean mathematics directed by a human-owned roadmap and gated by open, adversarial review: mathematicians choose the targets, AI agents author the proofs, and AI reviewers judge every pull request against open rubrics before it can merge. Current roadmap themes include universal covers, the Jacobian challenge, reductive algebraic groups, and partial differential equations.

Hex is a growing family of verified computational algebra libraries built with spec-driven development: we write the specifications, and AI agents implement both the executable code and the formal proofs. The results are already competitive with the unverified state of the art.

Palomar is a registry of Lean-verified mathematical results: it records claims from fixed versions of their source files, checks the proofs with Lean, and publishes the exact statement, the libraries it depends on, and the review comments. As the volume of AI-generated mathematics grows, an authoritative record of what has actually been verified becomes essential.

Over the next six months we will continue investing in all three projects: growing Tau Ceti’s library and roadmap, releasing further Hex libraries, and expanding Palomar’s coverage and community submissions.

Compiler🔗

Lean features a capable optimizing code generator, but essential improvements are still outstanding. Improvements include: better performance, stack-allocated objects, recursive join points, uniqueness annotations, and better support for array manipulating programs. These are deep changes, and rushing them would be a mistake. In this period we will focus on the design, and start the implementation at the beginning of 2027.

We will not invest in debugger infrastructure at this time. Debugger support is a recurring ask, but AI agents are changing how people debug code: they are already very effective at isolating bugs and proposing fixes, and this trend is accelerating. Investing in debugger infrastructure now would spend scarce compiler engineering time on a capability that matters less every month.