Incompressible strings, and Kolmogorov complexity is not computable

DefinitionPadding a string to a given length#✓fully proved

For a natural number \(n\) and a binary string \(p\), the padding of \(p\) to length \(n\) is the string \(0^k 1 p\) with \(k = \max(n - 1 - |p|, 0)\); when \(|p| < n\) it has length \(n\).

def pad (n : ℕ) (p : List Bool) : List Bool := List.replicate (n - 1 - p.length) false ++ true :: p

Used by 1

Used byFew strings have small complexity

TheoremFew strings have small complexity#✓fully proved

Fewer than 2 ^ m strings have complexity below m. Padding their shortest descriptions to length m maps them injectively to strings of length m other than 0ᵐ.

theorem card_lt_two_pow {m : ℕ} (S : Finset (List Bool)) (hS : ∀ x ∈ S, K x < m) :
    S.card < 2 ^ m

Uses 4 · Used by 2

Statement usesKolmogorov complexity

Proof usesThe universal description method · Shortest descriptions exist · Padding a string to a given length

Used byMost strings are incompressible · Incompressible strings exist at every length

DefinitionBinary strings of a given length#✓fully proved

For a natural number \(n\), the finite set of all binary strings of length \(n\).

noncomputable def stringsOfLength (n : ℕ) : Finset (List Bool) :=
  (Finset.univ : Finset (List.Vector Bool n)).map
    ⟨List.Vector.toList, List.Vector.toList_injective⟩

Used by 2

Used byMost strings are incompressible · Incompressible strings exist at every length

TheoremMost strings are incompressible#✓fully proved

For all natural numbers \(n\) and \(c\), fewer than \(2^{n-c}\) binary strings of length \(n\) have Kolmogorov complexity less than \(n - c\), where \(n - c\) is read as \(0\) when \(c > n\).

Hence at least \(2^n - 2^{n-c} + 1\) strings of length \(n\) have complexity at least \(n - c\).

theorem card_compressible_lt (n c : ℕ) :
    ((stringsOfLength n).filter fun x ↦ K x < n - c).card < 2 ^ (n - c)

Uses 3

Statement usesKolmogorov complexity · Binary strings of a given length

Proof usesFew strings have small complexity

TheoremIncompressible strings exist at every length#✓fully proved

Some string of length n has complexity at least n.

theorem exists_incompressible (n : ℕ) : ∃ x : List Bool, x.length = n ∧ n ≤ K x

Uses 3 · Used by 3

Statement usesKolmogorov complexity

Proof usesFew strings have small complexity · Binary strings of a given length

Used byKolmogorov complexity is not computable · The incompressible strings are not recognizable · Kolmogorov complexity is not lower semicomputable

TheoremKolmogorov complexity is not computable#✓fully proved

The function sending each binary string \(x\) to its Kolmogorov complexity \(K(x)\) is not computable: no partial recursive function, acting on binary strings through their encodings as natural numbers, halts on every binary string \(x\) with output \(K(x)\).

The proof is a form of Berry's paradox.

theorem not_computable_K : ¬Computable K

Uses 3

Statement usesKolmogorov complexity

Proof usesOptimality (the invariance theorem) · Incompressible strings exist at every length

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.