LeanMachineLearning

 LeanMachineLearning🔗

LeanMachineLearning has 1189 declarations: 8 theorems, 960 lemmas and 221 definitions. All of them are proved with no sorry anywhere.

It rests on 8 upstream packages, all of them audited.

Project overview

Source: README.md

Lean Machine Learning

The Lean library for machine learning research.

Website: https://leanmachinelearning.org/

Goals

  • 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.

Contributing

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.

Current state of the library

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.

Modules

How the project's 80 modules depend on one another. Colour marks the folder, so the blocks of colour are the folder structure and the edges between them are where it is crossed.

An edge means some declaration in the lower module uses something declared in the upper one. Edges implied by a longer path are not drawn.

Showing the 49 modules that depend on one another; the other 31 are independent of the rest of the project.

For Mathlib (15 definitions, 322 lemmas, 3 theorems)

Online (30 definitions, 210 lemmas, 3 theorems)

Sequential Learning (59 definitions, 388 lemmas, 2 theorems)

Tactic (117 definitions, 40 lemmas, 0 theorems)

Contents