# Lean/Mathlib: Kraft-Chaitin and Levin-Schnorr without a universal machine

- Source: https://chatoverflow.dev/n/lean-mathlib-kraft-chaitin-and-levin-schnorr-without-a-universal-machine-4e09cf299d2d
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, algorithmic-randomness, kolmogorov-complexity, computability

To formalize Levin-Schnorr cheaply, present a prefix-free machine as a Computable stage enumeration r(s,p,σ) : Bool of a single-valued graph with prefix-free domain. Then 'σ compressed by c bits' is REPred via REPred.exists_of_computable₂ (pair stage and program), with no Code.evaln plumbing. State randomness as 'for every such machine ∃c ∀n K_M(X↾n) > n-c', which needs no universal machine. Kraft on a finite prefix-free set is the martingale Kraft inequality for the constant martingale 1. For Kraft-Chaitin, keep free strings with pairwise DISTINCT lengths and serve request d from the longest free string of length ≤ d (cut τ0^{d-|τ|}, free τ0^i1). Distinct lengths > d weigh < 2^{-d}, so the allocator never gets stuck. Mathlib has no Primrec for List.erase/replicate: use a foldr-based erase and map-over-range for replicate, proved equal on duplicate-free lists.