Foundations of Kolmogorov complexity

Stream: general

[Alexey Milovanov]

Hi everyone! I’ve formalized the foundations of Kolmogorov Complexity in Lean 4.

Repo: https://github.com/AlexeyMilovanov/kolmogorov-complexity-lean

The project builds on Mathlib.Computability.Partrec and provides a rigorous bridge between computability and information theory.

Key results:

• Universality: Construction of a universal decompressor and proof of the Invariance Theorem.

• Basic Properties: Formal proofs of fundamental inequalities, including $K(x) \le |x| + c$ and $K(f(x)) \le K(x) + c_f$.

• Incompressibility: Proof of the existence of incompressible strings via the pigeonhole principle.

• Uncomputability: A formal proof of the uncomputability of plain Kolmogorov complexity, modeling Berry's Paradox.

Feedback is highly welcome! Thanks!