Lean Machine Learning
Lean Machine Learning
The Lean library for machine learning research
Lean Machine Learning is a carefully curated library of formalized definitions and theorems in machine learning theory, verified in Lean.
Repository
Tutorials
Roadmap
Zulip
API Docs
Documentation
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.
Inside the Library
A snapshot of what is formalized today. The library is young, and every part of it is open to contributions.
Algorithms and Environments
A framework for stochastic sequential algorithms: policies and environments as Markov kernels, and the probability space carrying their interaction over time.
Bandit Regret Bounds
Explore-then-commit, upper confidence bound and Thompson sampling, each defined in that framework and each with a proved bound on its regret.
Kernels and Tactics
Probability and Markov kernel material headed for Mathlib, together with two tactics that automate the bookkeeping of kernel manipulations.
Formalized with Lean Machine Learning
A selection of research papers that have been formalized using the Lean Machine Learning library.
On Response-Adaptive Targeting Strategies for Multi-Treatment Experiments
Yagouti et al., 2026, preprint.
Formalization: https://github.com/RemyDegenne/alpha-rar
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.
Maintainers
