Website: https://leanmachinelearning.org/

• A library of high-quality formalization of machine learning definitions.
• Essential theorems and proofs in machine learning theory.
• A framework for working on machine learning algorithms in Lean.
• An extensive documentation, with examples and tutorials.
• A trusted basis for formalization of machine learning research.

Please see our contribution guide and code of conduct.

For discussions, you can reach out to us on the Lean prover Zulip chat.

You can also see the roadmap for ideas on what to work on.

As a first proof of concept, the repository contains a formalization of regret bounds for several stochastic bandit algorithms.

Main results:

• Framework for working on (bandit) algorithms in Lean.
• Regret bound for the Explore-Then-Commit algorithm.
• Regret bound for the UCB algorithm.