The Lean FRO Year 3 Roadmap

Our roadmap for the third year of Lean FRO operations from August 2025 - July 2026.

Vision

The Lean Focused Research Organization (FRO) envisions a future where Lean, a proof assistant and open-source programming language, becomes a pivotal tool in driving innovation and progress across diverse fields. Our vision extends to formal mathematics, software and hardware verification, software development, AI research for mathematics and code synthesis, and new math and computer science education methodologies. We are dedicated to fostering a dynamic, decentralized ecosystem that thrives on diversity and collaboration. We support Lean's growth by engaging with a global community, encouraging open-source contributions, and forging educational partnerships, ensuring our efforts resonate widely. We aim to make Lean an indispensable resource for researchers, developers, educators, and students. We are now in our third year as a FRO starting in August of 2025.

Mission for Year 3

Year 3 completes foundational work begun in Years 1–2, with special emphasis on proof automation and aggressive compiler performance work.

Key objectives

  1. Finalize Std; support Mathlib maintainers in reducing technical debt.

  2. Ship next‑generation proof automation: grind, scalable simp, counter‑example generation, and rich diagnostics.

  3. Deliver major compiler performance gains (new backend, significantly smaller binaries).

  4. Land new do-notation and related language‑frontend features for verification condition generation and async/await.

  5. Provide reliable benchmarking, testing, and profiling infrastructure for Lean and Mathlib.

  6. Close the usability gap: formatter, clearer error messages, IDE polish.

  7. Demonstrate Lean’s prowess in multiple domains.

Year 3 Deliverables

1. Standard Library

Description: The standard library (Std) underpins all Lean programs and libraries. It is the critical foundation upon which the rest of the Lean ecosystem is built, enabling consistent interfaces and reliable core functionality.

Strategy: Our plan is to complete the remaining essential modules—including containers, networking, and asynchronous I/O—and to finalize and document the API. By July 2026, Std will be a stable foundation for future development.

Deliverables: We will publish a release candidate for Std version 1.0, which will include all fundamental modules fully specified and verified. This release will feature support for async/await primitives and a new HTTP server library. Additionally, we will produce an updated document outlining the intended scope of Std along with a policy for maintaining stability going forward.

2. Benchmark & Test Suite

Description: To ensure Lean’s long-term stability and performance, we are creating a unified system for benchmarking and regression testing that will serve as a central observability layer across core tooling.

Strategy: This initiative involves building a comprehensive test and benchmark suite, along with an enhanced public dashboard that tracks performance trends over time. Through this, we aim to make performance improvements and regressions visible and actionable.

Deliverables: The dashboard will display daily performance runs, highlighting trends and regressions. The system will include a targeted micro-stress test suite that exercises the kernel, elaborator, and key tactics (simp, grind, bv_decide). We will also include end-to-end case studies demonstrating performance in real-world contexts (see item 7), and we will integrate reproducible benchmark CI pipelines across all core repositories.

3. Language Frontend & Developer Experience

Description: This workstream focuses on improving the core user-facing language features, including the new do-notation, module system enhancements, and tools that make development smoother—such as formatting, caching, and clearer error feedback.

Strategy: Following the deployment of the new code generator in June 2025, we will implement a modernized do-notation that enables verification condition generation and supports async workflows. We also plan to roll out a code formatter to ease collaboration in large projects and introduce caching mechanisms for computationally expensive tactics.

Deliverables: We will release a new do-notation that integrates seamlessly with verification workflows and introduces async/await syntax. Caching support will be added for terminal tactics, dramatically speeding up iterative proof development. Work will continue on improving error messages and diagnostics. We will also complete support for coinductive predicates and advance improvements to the module system for better structure and encapsulation.

4. Proof Automation

Description: This line of work aims to make Lean's automated reasoning tools significantly more powerful, efficient, and broadly applicable, especially in high-performance verification and formal methods settings.

Strategy: We are improving the performance and expressiveness of Lean's main automation tactics, including grind  and simp. This includes fixing performance bottlenecks, extending support for reasoning about orders and nonlinear arithmetic, and integrating new arithmetic normalizers. We are also responding to user feedback to enhance the usability and coverage of grind. In parallel, we are developing improved diagnostics to help users understand what the automation is doing and why. Additionally, we are working on a counterexample generator to complement proof automation with early error detection capabilities.

Deliverables: We will deliver updates to grind and simp with extensive performance improvements and new reasoning features, enabling their application to large-scale software and hardware verification tasks. We will also unify existing rewriting tactics, such as rw and simp_rw, into a single, more intuitive and powerful rewrite tool. A next-generation simplifier, inspired by simp but designed to scale to industrial use cases, will be engineered and released. Finally, we plan to release an MVP of a counterexample generator to help detect incorrect assumptions and implementation bugs early in the development cycle.

5. Language Backend

Description: We are redesigning the backend infrastructure—especially the code generator—to produce smaller, faster binaries and to scale with large inductive types and complex recursive definitions.

Strategy: Efforts are focused on improving the scalability of constructions like noConfusion, completing derived instances for equality and ordering, and refining the performance of match expressions. The centerpiece is completing and evolving the new code generator to support stack allocation, better reference-counting, and ownership-aware compilation.

Deliverables: We will deliver more scalable implementations of key constructions, including noConfusion and derivable instances for DecidableEq, BEq, Repr, and Ord. Missing deriving handlers—such as for LawfulBEq, TotalOrd, and StrictWeakOrd—will be implemented. Improvements to match expression handling will make it more robust and scalable. Nesting induction through collections such as HashMap and TreeMap will be supported. The new code generator will include support for stack-allocated objects, ownership annotations, and improved placement of reference-counting instructions.

6. IDE & Tooling

Description: We are refining the Lean developer experience through sustained improvements to IDE tooling, build systems, and interoperability layers such as the FFI.

Strategy: Our focus is on polishing the VS Code extension, filling remaining gaps in the LSP implementation, and stabilizing Lake. We also aim to define minimal but effective guidelines for FFI use and provide example bindings in multiple languages.

Deliverables: A fully integrated code formatter will be available within the VS Code extension, which we will continue to maintain actively. Support for improved, general cloud caching will be integrated into Lake/Reservoir, and versioning support will be added to Lake. We will also publish basic FFI guidelines and provide sample bindings in C, Rust, and Python to demonstrate Lean’s ability to interoperate with external systems.

7. Case Studies

Description: These case studies will demonstrate Lean’s maturity and utility by applying it in real-world contexts, particularly in software and hardware verification.

Strategy: We plan to develop multiple high-impact, end-to-end case studies that showcase Lean’s strengths. Each will focus on a concrete problem and highlight both challenges and solutions.

Deliverables: Each case study will be published as a public repository, accompanied by detailed write-ups explaining the approach, methodology, and insights gained. Together, they will serve as concrete evidence of Lean’s readiness for serious applied work.

8. Literate Programming & Next‑Generation UX

Description: This multi-year initiative seeks to make Lean more approachable and usable by investing in mixed formal/informal document authoring tooling and creating a rich, web-first user experience.

Strategy: We will continue and extend development of tools like Verso, prototype a new DSL for scientific communication, improve online interfaces, and lay the foundation for Lean-based educational experiences.

Deliverables: Verso will be enhanced to support both PDF extraction and interactive website generation. A new DSL—LaTeX-inspired and tailored for Lean—will be prototyped to support scientific writing. Improvements will be made to the usability and administration of the live.lean-lang.org playground software. We will also release an MVP for the Lean Online Platform as a web-only UI solution with secure sandboxing, author a user guide for literate Lean authoring, and release an initial version of a revamped, basic framework for educational Lean games.