Lean Machine Learning
Goals & Features
Lean Machine Learning is building a foundation for formalized machine learning theory. You proved that your new algorithm converges at the optimal rate and your LLM formalized the proof. Lean checked the proof. But who checked the Lean definition of optimal rate? We did. Since your LLM is using a Lean Machine Learning definition, you can trust it proved the right thing.
Formalized Definitions
Rigorous definitions of machine learning concepts: algorithms, performance measures, etc. All the tools needed to talk about machine learning theory.
Proven Theorems
Essential theorems in machine learning theory. Convergence guarantees, regret bounds, and foundational results in probability theory and optimization.
AI-Ready
A common vocabulary of formal definitions that can be used by AI systems to generate theorems about objects we care about and avoid misformalization errors.
Algorithmic Tools
A framework for defining and analyzing stochastic algorithms in Lean, and to connect formal specifications with executable implementations.
Documentation
Comprehensive documentation with examples and tutorials to guide users through the library and its applications.
Collaborative
Open source, collaborative, and integrated in the Lean ecosystem. We welcome contributions from the community. We build on top of Mathlib and contribute to it in return.
Sponsors and Partners
We are grateful for the support of the following organizations.
Inria FORMAL exploratory action
If you are interested in supporting Lean Machine Learning financially please reach out to Rémy Degenne at remy [dot] degenne [at] inria [dot] fr or on the Lean Zulip (preferred).
Maintainers
