arlib

A Lean 4 + Mathlib library of reusable results in randomised algorithms and their analysis: finite probability and concentration, approximate counting and sampling, Markov chain mixing, knowledge compilation and circuit size lower bounds, communication complexity, automata state lower bounds, information theory, finite MDPs, and coresets. It is written the way Mathlib is written — general statements, one namespace per module path, a docstring on every declaration.

Currently 310 modules and roughly 115,000 lines, sorry-free, and dependent on no axiom beyond the three Mathlib itself uses.

What's inside

Twelve areas, in dependency order: Prelude, Combinatorics, Communication, Probability, InformationTheory, MarkovChains, Approximation, MDP, GameTheory, Algorithms, KnowledgeCompilation, Automata.

Each is a directory Arlib/<Area>/ with an area root Arlib/<Area>.lean that re-exports it. import Arlib gives you everything; import Arlib.MarkovChains gives you one area; importing a single module gives you one piece.

ARCHITECTURE.md § 1 has the table: what each area contains and how large it is, with § 3 expanding every area into a module-by-module map. The area roots themselves carry the real documentation — each is a long docstring on what its subject is for and how it is organised.

Getting started

arlib is not tied to a fixed Lean release: it follows Mathlib, and the Mathlib revision it is currently built against is locked in lake-manifest.json. The one place a Lean version is written down is lean-toolchain, which must match Mathlib's own — today that is:

leanprover/lean4:v4.33.0

Your project must use the same toolchain, so copy that line into its lean-toolchain, then add arlib to your lakefile.toml:

[[require]]
name = "arlib"
git = "https://github.com/meelgroup/arlib.git"
rev = "main"

If you prefer SSH, use git = "git@github.com:meelgroup/arlib.git" instead. arlib requires Mathlib itself, so you do not need to require Mathlib separately unless you want to pin it yourself — if you do, pin it to the revision in arlib's lake-manifest.json.

Then:

lake exe cache get   # fetch prebuilt Mathlib oleans
lake build

Always run lake exe cache get first. Without it, Lake will compile Mathlib from source, which takes hours.

A worked example

Finite probability in arlib is deliberately elementary: a FinProb is a finite outcome type with an explicit mass function, events are Finsets, probabilities are real sums, and everything is decidable. That is what lets combinatorial arguments go through with no measure theory.

import Arlib.Probability

open Arlib.Probability Arlib.Probability.FinProb

/-- A fair coin. This is the whole interface: a finite outcome type `Ω`, and a
law on it — a nonnegative mass function summing to one. -/
noncomputable def fairCoin : FinProb where
  Ω := Bool
  μ :=
    { p := fun _ => 1 / 2
      p_nonneg := by intro _; norm_num
      p_sum := by simp }

example : fairCoin.Pr {true} = 1 / 2 := by
  simp [FinProb.Pr, FinProb.mass, fairCoin]
  rfl

/-- The union bound over a `Finset` of events — the workhorse of the area. -/
example (P : FinProb) (s : Finset ℕ) (E : ℕ → P.Event) :
    P.Pr (s.biUnion E) ≤ ∑ i ∈ s, P.Pr (E i) :=
  P.Pr_biUnion_le s E

Documentation

• ARCHITECTURE.md — the structure of the library: every area, every directory, and § 5 on the results imported from the literature as explicit hypotheses rather than proved here, with the theorems that take each one.
• CONVENTIONS.md — the house style: naming, namespacing, statement shape, docstrings, and the standing design commitments.
• CONTRIBUTING.md — how to build, test, audit and submit.
• CONTRIBUTORS.md — who wrote what, and how authorship is recorded.
• REFERENCES.md — every paper the library formalizes or cites, with the short key used in the docstrings. Its last section, Known gaps, lists the places where a result is stated without its source; those are outstanding defects, and one of them covers a whole area.
• The area roots (Arlib/Probability.lean, Arlib/MarkovChains.lean, and so on) are the real reference. Each carries a substantial docstring explaining what the area is for, how it is organised, and what its conventions are, with a module-by-module table. Working notes and statement-by-statement paper inventories live under docs/dev/.
• API documentation is generated by doc-gen4 in CI from the default branch.

Versioning and stability

arlib is pre-1.0 and there is no stable API. Names move, namespaces are normalized, and lemmas are hoisted between modules as the library is consolidated. If you depend on it, pin a specific commit.

Every rename is recorded in MIGRATION.md, old name to new name, so an upgrade is a mechanical edit rather than a search.

Citing

@software{meel2026arlib,
  author = {Meel, Kuldeep S.},
  title  = {arlib: a Lean 4 library for randomised algorithms and their analysis},
  year   = {2026},
  url    = {https://github.com/meelgroup/arlib}
}

License

Released under the Apache License 2.0, following Mathlib.

Copyright © 2026 the arlib contributors. The per-file headers are authoritative for who holds copyright in which module.

Origins

arlib was started by Kuldeep Meel, and has since evolved with contributions from Suguman Bansal and Uddalok Sarkar. See CONTRIBUTORS.md for who wrote what.

It was distilled from formalization projects in author's works, where the same probability and combinatorics infrastructure had been copy-pasted, with drift, across several developments. Those copies were deduplicated, re-namespaced and generalised into what is here.

Acknowledgements

Built with the assistance of Claude (Anthropic's Claude Code).