Lean FRO Year 1 in Review

Year 1 Mission and Priorities

Our laser-focused first-year goals fell into eight categories, from improving Lean’s core system and proof automation capabilities, documentation, and resources to laying the foundation of our standard library and launching Lean’s package repository, Reservoir. Overall, we aimed to increase Lean’s speed and usability and architect for long-term scalability.

In parallel, we sought to hire a team with deep expertise in formal methods and mathematics to develop and maintain Lean, and augment and support the work of the Lean community. Finally, we embraced our first year as a non-profit Focused Research Organization (FRO) within Convergent Research by setting our mission, establishing key operational and financial infrastructure, and forming our Board of Directors and Strategic Advisory Board.

Summary of Results

We are pleased with our progress against our year 1 roadmap and establishing Lean FRO as the organizational engine for Lean's long-term success. With each release of Lean this past year we have improved the system's capabilities and value to its users.

We have been most excited to see Lean contribute to impressive advancements in mathematics, HW/SW verification, AI, and math and CS education. Noteworthy examples in mathematics include Terence Tao's project formalizing the Polynomial Freiman-Ruzsa (PFR) conjecture, Kevin Buzzard's public project to prove Fermat's Last Theorem in Lean, and Floris van Doorn's launch of the Carleson project, which aims to formalize Carleson's theorem.

In the area of HW/SW verification, AWS’s integration of Lean with Cedar to achieve software verification at the highest level of correctness and use of SampCert in the AWS Clean Rooms Differential Privacy service are key examples of Lean adoption within the commercial sector. At the intersection of math and AI, Terence Tao’s Scientific American interview and Oxford Mathematics lecture about Lean and other theorem provers’ contributions to these fields, Harmonic’s announcement of their Mathematical Superintelligence Platform, and DeepMind’s silver medal performance at the International Mathematical Olympiad stand out.

Our academic community has continued to build out courses using Lean, and we’ve seen a steady uptick in academic papers and other assets that support teaching and learning in Lean. More talks and presentations by Lean users have been given than we can list here, and we were also invited to give talks at events including Bobkonf, SSFT, and the International Conference on Computer Aided Verification (CAV).

These achievements illustrate increasing engagement, contributions, and success from mathematicians, researchers, and developers across academia and industry.

Here is a summary of key results we have realized since July 2023:

• Hired eleven Lean FRO team members, established our Board of Directors and recruited our Strategic Advisory Board. We have also secured enough funding from our donors to ensure Lean is on a strong path towards self-sufficiency.

• Implemented key architectural changes to make Lean faster, simpler, and more robust. Highlights include upstreaming a large part of the Std library into Lean, creating a separate community library for additional contributions (batteries), and launching Reservoir, the Lean package repository, and integrating it with Lake, the Lean build tool.

• Improved support for incremental proof processing and reasoning about recursive functions and bitvectors, including our verified bitvector decision procedure. The new omega tactic implements an important decision procedure for integer linear arithmetic.

• Created a capable authoring tool - Verso - dedicated to producing high-quality Lean documentation.

• Launched our blog series, supported by detailed release notes, to improve and streamline communications.

• Closed 406 issues on GitHub, merged 1545 PRs, and implemented over 900 improvements to Lean.

• Embraced a partner-first model for increasing Lean’s value in AI and ML, including providing support for Harmonic, investing in an upcoming expansion of Moogle, and welcoming opportunities to help train popular, open-source LLMs against Lean data.

• Deepened our relationships with academic institutions and researchers, including Sean Welleck’s L3 Lab and Jeremy Avigad’s Hoskinson Center at CMU. We also offered technical support and guidance for multiple papers, academic institutions, and grant proposals related to Lean, including a number at the intersection of math and AI.

Tracking Progress

In Year 1, we measured Lean’s success across five metrics: Monthly Active Users (MAU), Number of Packages, Number of Courses, Proof Verification Time (PVT), and Overhead Factor. The first three metrics showed clear improvements, with results of +49%, +372%, and +89% YoY, respectively. Proof Verification Time - the time required to compile and check one million lines of Lean code - has been a more complex metric to optimize. We are working to adjust this metric to better segment our analysis and determine actions. We are also exploring replacing Overhead Factor - which cannot be calculated reliably - with a different measure of proof automation productivity.

Key Learnings

Our first year as a FRO was a journey of learning and growth, largely shaped by the invaluable contributions of our Mathlib community. We encountered challenges with Mathlib’s efficiency, such as multiple regression issues and a backlog of technical debt. These hurdles prompted us to implement architectural changes and increase our expert resources within the FRO. We deeply appreciate the active involvement of our Mathlib contributors and maintainers, and we are committed to accelerating its usefulness, speed, and quality. Year 2 will see a heightened focus on and investment in Mathlib.

More broadly, we could have made more progress in reducing papercuts across the Lean system and responded faster to new user issues. A few essential resources, including our reference manual, still need to be completed. Some of our technical challenges directly resulted from improvements we made in Lean. Still, we needed better systems and processes for triaging and resolving issues and PRs, and began allocating more time and resources to this work over the past quarter. We will continue to increase our rigor and investment in resolving high-priority issues, reducing papercuts, and providing key user resources in Year 2.

We also need to invest in programs to support our different audiences better. For example, there is a rich but disconnected body of teaching and learning resources built by the Lean community, including courses, textbooks, tutorials, videos, games, and other assets. We love seeing these materials emerge across the globe - it is a testament to the robustness of our community - but we need to help curate, improve, and evangelize the content that best supports Lean students and users. Commercial users have similar but slightly different needs that we also need to meet. Year 2 will see investments in scalable programs focused on better serving the needs of our audiences along with a relaunch of our website to provide easier access to resources and tools.

The Road Ahead

We are excited to build on the foundation of the last twelve months and further improve Lean’s system in terms of scalability, usability, documentation, and proof automation. Beyond our technical roadmap, Lean FRO will refine the strategy and build the capabilities needed to support and grow our communities of Lean users and steer Lean towards self-sustainability, laying a strong foundation for its enduring growth and widespread utilization.

Please see our year 2 roadmap for more details.

Thank You

As we close out our first year as Lean FRO, we thank the dedicated and growing global community of Lean contributors, our Lean FRO team members, our industry partners, and the community of researchers, educators, and students who are making Lean better today and paving the way for the next generation of users.

We would not be celebrating this milestone without the generosity of our donors - Simons Foundation International, the Alfred P. Sloan Foundation, Richard Merkin, and Founders Pledge - and the team at Convergent Research, whose advocacy and support are critical for us to achieve long-term self-sustainability for Lean. Special thanks go to our Board of Directors and Strategic Advisory Board for their vision and guidance.