The Lean Focused Research Organization envisions a future where Lean drives innovation and progress across formal mathematics, software and hardware verification, software development, AI research for mathematics and code synthesis, as well as new math and computer science education methodologies.

We support Lean's growth and impact by engaging with the global community, encouraging open-source contributions, and forging educational partnerships.

We aim to foster a dynamic, decentralized ecosystem thriving on diversity and collaboration to ensure Lean is an indispensable resource for researchers, developers, educators, and students.

Our 5-year mission is to advance Lean's critical systems and capabilities, expand its influence and to steer Lean toward long-term self-sustainability. Critical areas of focus include:

• Scalability enhancements
• Usability improvements
• Advancements in proof automation
• Improving documentation and documentation generation tools
• Increasing application accross diverse fields
• Building a diverse and inclusive community
• Supporting AI research and verified code synthesis

Read our current roadmap for more details on our planned initiatives.