LeanMachineLearning

 LeanMachineLearning🔗

What would it take to believe this library?

LeanMachineLearning states 6 results as theorems and proves all 930 of its declarations with no sorry anywhere.

Believing them means also accepting 8 upstream packages, of which 0 are unaudited.

Every declaration here carries what it claims, what it rests on, and a single self-contained Lean file holding everything you would have to read to check it.

The results, largest first by how much machinery they rest on.

  • Bandits.TS.integral_regret_le23 beneath

    If Thompson sampling has the correct prior over environments and every environment has K actions, each of which has a corresponding reward between l and u that is sub-Gaussian with variance proxy σ2 after its mean is subtracted, then the Bayesian regret at time n is at most (2 * K + 1) * (u - l) + 8 * √(σ2 * K * n * Real.log n).

  • Bandits.UCB.regret_le20 beneath

    Regret bound for the UCB algorithm.

  • Bandits.ETC.regret_le18 beneath

    Regret bound for the ETC algorithm.

  • Learning.randomSampling.action_tendsto_any10 beneath

    The minimum distance from sampled actions to any point tends to zero.

  • Learning.IsAlgEnvSeq.identDistrib_trajectory5 beneath

    The law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

  • Finset.measurable_inf'0 beneath

    Dual version of Finset.measurable_sup'.

See all claims.

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 68 modules depend on one another. Colour marks the chapter, so the blocks of colour are the chapter 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 47 modules that depend on one another; the other 21 are independent of the rest of the project.

For Mathlib (6 definitions, 143 lemmas, 1 theorems)

Online (31 definitions, 195 lemmas, 3 theorems)

Sequential Learning (56 definitions, 336 lemmas, 2 theorems)

Tactic (117 definitions, 40 lemmas, 0 theorems)

Contents