The Lean FRO Year 2 Roadmap

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 second year as a FRO, and our original roadmap is here.

Mission

Our mission is to enhance the Lean system in critical areas: scalability, usability, documentation, and proof automation, while also broadening its application in various fields such as education, research, and industry. Over the next four years, we are dedicated to advancing Lean's capabilities and expanding its influence. A pivotal aspect of our mission is to steer Lean towards self-sustainability, laying a strong foundation for its enduring growth and widespread utilization.

  • Scalability Enhancements: Our goal is to optimize Lean for handling increasingly complex and large-scale projects, such as Mathlib, ensuring it meets the demands of advanced computational and analytical tasks in various domains.

  • Usability Improvements: We aim to make Lean more intuitive and user-friendly, enhancing its interface and functionality to cater to a wide range of users, from mathematicians and software developers to verification engineers, AI researchers, and the academic community.

  • Advancements in Proof Automation: By improving automation, we aim to decrease formalization overhead and make writing verified programs and mathematical proofs easier.

  • Documentation and Documentation Generation Tools: Committing to high-quality, easy-to-use documentation, we will develop and provide advanced documentation authoring tools alongside traditional resources. This will facilitate the creation of user guides, tutorials, best practices, and detailed technical documentation. We aim to ensure that these resources are thorough and clear, continuously updated, and easy to navigate for all users, from beginners to advanced practitioners in various disciplines.

  • Broad Application in Diverse Fields: We are dedicated to demonstrating Lean's utility and adaptability in a variety of sectors. Our focus extends equally to formal mathematics, software and hardware verification, AI research for mathematics and code synthesis, and innovative math and computer science education methodologies. By showcasing Lean's versatility, we aim to establish it as a valuable tool in each of these domains, and we believe that tools developed in one domain will improve the experience of users working in other domains.

  • Building a Diverse and Inclusive Community: We are committed to fostering a dynamic, inclusive community around Lean. This involves engaging with stakeholders from academia, industry, and educational sectors to create a decentralized network of collaboration and innovation.

  • AI Research and Verified Code Synthesis: We aspire for Lean to become an indispensable tool in AI research, particularly in mathematics and verified code synthesis. Lean is an ideal target language for generative AI. Its expressive logic provides a unique training environment for logic and reasoning. Lean enables trustworthy AI-driven code synthesis by allowing models to generate both code and proofs of specifications.

  • Steering Towards Self-Sustainability: A critical aspect of our mission is establishing a sustainable operational and financial model for Lean. This will involve developing strategies for long-term funding, community support, and organizational growth, laying the groundwork for future independence and self-sufficiency.

Furthermore, we aim to transition to a foundation model similar to the Rust and Linux Foundations. This transition will mark a significant step in establishing Lean as a widely supported tool, laying the groundwork for its continuous growth and evolution.

Year 2 Deliverables

As we chart our course for the next four years, the Lean FRO is committed to developing and enhancing key components integral to the Lean ecosystem. This section outlines these deliverables.

Preamble: Involvement of External Contributors

We warmly welcome external contributors to participate in the exciting journey of growing and improving Lean. It's important to note that while there are numerous opportunities for contributors at various levels of expertise, certain critical components require a deep understanding of Lean and a strong track record of reliability. Our core team must carefully prioritize using scarce time on contributor mentorship versus direct technical work. Therefore, we encourage new contributors to start with less critical components, which are excellent entry points to get acquainted with Lean's development process and build technical knowledge and trust with the Lean FRO development team. As contributors gain experience and demonstrate their skills, there will be opportunities to engage with more complex and critical parts of the Lean system.

1. Package Management

Description: Besides serving as a traditional package registry for Lean, Reservoir aims to be a significant leap forward in managing and facilitating package compatibility and development. Its design goes beyond mere package storage and distribution, serving as a comprehensive breakdown of Lean's ecosystem.

Year 2 strategy: In Year 2, we will improve Lean’s package management by building new infrastructure for use by community and industry partners alike.

Deliverables: Our priority deliverables in Year 2 are to: complete our Cloud cache, provide support for Private registry, deliver an interface and support for private build systems (e.g., Google’s Bazel, AWS’s Brazil), and resolve FFI paper cuts.

2. Mathlib

Description: The Lean mathematical library, Mathlib, is a community-driven effort to build a unified library of mathematics formalized in Lean. The library also contains definitions useful for programming. As of June 2024, Mathlib has received contributions from over 300 mathematicians and contains 1.56M lines of code, more than most other formal mathematics systems.

Year 2 strategy: Our focus this year is to augment and support the priorities of the Mathlib maintainers and broader Mathlib community with Lean FRO employees. We will also invest Lean FRO resources in reducing Mathlib’s technical debt to improve its speed and efficiency.

Deliverables: This year our goals are to: deliver a benchmark suite based on Mathlib in core, execute a technical debt elimination plan that enables growth to 10M LoC, implement an improved Pull Request process, and provide critical support for Kevin Buzzard’s Fermat’s Last Theorem project.

3. User Interface

Description: Our user interface is the gateway for Lean users, so it must be intuitive, easy to navigate, and error-free so that new and experienced users alike can maximize the value of their time programming in Lean.

Year 2 strategy: Building on top of technical debt reduction in Year 1, we plan to thoroughly improve and extend our language server and editor extension.

Deliverables: To achieve our goals, we will implement multiple performance improvements, revamp auto-completion, and improve the new user experience (UX).

4. Language frontend

Description: The frontend is the textual interface of Lean, ranging from the parser to the elaborator and tactic framework. It is the central workhorse of Lean and, thus, a main focus of further optimization work.

Year 2 strategy: In Year 2, we aim to improve system responsiveness. Parallelism will reduce both build times and editor latency. We expect the module system will improve recompilation times, and phase separation will reduce the binary size for Lean applications.

Deliverables: This year we will provide support for parallelism and structure command, and resolve structure instance issues. We will also create a module system, enable phase separation, and provide support for skipping expensive tactics.

5. Documentation

Description: A key focus for Lean FRO in Year 1 was the development of a comprehensive Documentation Authoring Tool - Verso. This tool is designed to be a one-stop solution for creating various Lean-related documents, including manuals, tutorials, lecture notes, and blog posts.

Year 2 strategy: Our plan is to ensure all Lean documentation is based on Verso.

Deliverables: In Year 2 we will deliver a comprehensive reference manual, port Theorem Proving in Lean and Functional Programming in Lean to Verso, and release a new version of Verso. We will also relaunch the Lean website with improved navigation and access to valuable content, resources, and tools.

6. Standard library

Description: We envision a standard library akin to Rust’s, but with specifications, proofs and tactics for its main components. The Lean standard library will also serve as the bedrock for many other packages and projects.

Year 2 strategy: This year, we will drive improvements to the Std library through additional resourcing and ensure it is part of the Lean distribution package.

Deliverables: To achieve our goal, we will deliver a document describing scope and vision for Std, provide support for Definitions and Theorems for all basic types, implement LeanSAT in core and provide support for other finite types. We will also provide support for http server library and async IO.

7. Language backend

Description: The backend encompasses the kernel, code generator, proof automation, and proof by reflection support.

Year 2 strategy: Our goals are to deliver SMT-like proof automation for dependent type theory, improve performance for software/hardware verification applications, extend LeanSAT support for finite types, and provide support for proof by reflection.

Deliverables: We will deliver Mutual/Nested structural recursion and induction principle, an improved simp theorem generation, a reduction engine in the kernel, SMT-like automation (grind), and kernel performance improvements. Bandwidth-permitting, we will also deliver a new code generator.

8. AI/ML

Description: Lean is used as the basis for automated theorem proving using Large Language Models (LLMs) and for automatic translation of prose theorems and proofs into formalized mathematics. Because Lean can mathematically verify the correctness of code, AI and ML developers can prove properties about their models, ensuring robustness and reliability.

Year 2 strategy: Our strategy is to embrace a partner-first model for increasing Lean’s value in AI and ML, supported by Lean FRO efforts. We will seek to provide tooling, data, and other support that enables AI organizations and researchers to advance Lean’s contribution at the intersection of AI, math, and science.

Deliverables: Our priority deliverables in Year 2 are to: develop a VS Code integrated chat assistant, support the expansion of Moogle 2.0 for code and documentation search, provide Lean datasets to Mistral and other partners. If we have resources and capacity, we will explore other contributions that are out of scope for academic and commercial entities.