kolmogorov_complexity

Formalized Algorithmic Information Theory in Lean 4

This repository contains a Lean 4 formalization of algorithmic information theory, built on Mathlib.

The main references are Alexander Shen, Vladimir A. Uspensky, and Nikolai Vereshchagin, Kolmogorov Complexity and Algorithmic Randomness (SUV), and Nikolai Vereshchagin and Alexander Shen, Algorithmic statistics: forty years later.

The development is based on Mathlib's computability infrastructure. Decompressors are represented as partial functions, finite objects are represented by bitstrings, and most theorem statements are phrased up to the additive or logarithmic slack terms natural in Kolmogorov-complexity arguments.

What Is Formalized

The SUV book: selected results on plain, prefix and monotone complexity, algorithmic probability and randomness, Shannon entropy, information inequalities, common information and multisource information theory.
Algorithmic statistics: finite-set and distribution models, stochasticity profiles, restricted descriptions and strong sufficient statistics, following the Vereshchagin-Shen survey.
Incompleteness: Chaitin-style and Kritchman-Raz-style results, using abstract formal-system interfaces rather than a concrete arithmetic system.
Further developments: Solomonoff induction, Solomonoff prediction of selected bits, the negative answer to Shen's question on the a priori probability of a prefix, stopping complexity, and the exact realisation of min(K, F) for an entropy function F by a prefix machine (Allender-Friedman-Gasarch, Claim 1), and the Allender-Friedman-Gasarch theorem that a decidable set polynomial-time reducible to the K_U-random strings for every optimal prefix machine U lies in EXPSPACE (resource-bounded machines, complexity classes and the game construction in KolmogorovMathlib/RandomStrings/).
New strong-merging results: the square-root merger of two strong sufficient statistics, its matching obstruction and the questions of survey Section 7.9.

The detailed overview lists the main theorems and their modules. The SUV coverage table records exactly which book items are covered and which are not.

Build

Install Lean through elan, then fetch the Mathlib cache and build the exported library target:

lake exe cache get
lake build KolmogorovMathlib

For the default package build — the library together with the counterexample library — run:

lake build

bash scripts/audit.sh is the completion gate (forbidden constructs, sorry scan, build, warning gate, co-import smoke test, axiom sweep, tactic smoke tests).

The SUV coverage table maps book items to theorems and is regenerated by scripts/gen_suv_coverage.py.

The HTML documentation is built from the side package docbuild/, which is the only place doc-gen4 is required, at a revision pinned to this repository's Lean release:

cd docbuild
lake update doc-gen4
lake build KolmogorovMathlib:docs KolmogorovCounterexamples:docs   # writes .lake/build/doc

.github/workflows/ci.yml runs the build, the audit, the test scripts under scripts/tests/ and the documentation build; scripts/ci_local.sh runs the same steps locally, and the workflow calls that script so the two cannot drift apart.

The library has a single build root, KolmogorovMathlib, which imports every module of the library, directly or through other modules: the root imports the maximal modules of the topic directories itself, and KolmogorovMathlib/Extras.lean, which the root also imports, collects the side modules outside the main development line (alternative developments, spare interfaces and side results), so that they stay in the build. KolmogorovCounterexamples is a second root, deliberately not imported by the library, and the release check builds it too.

This branch is pinned to Lean v4.35.0 and the matching Mathlib ecosystem.