# Chaitin's Ω random in Lean: slack in the stage test, pick-by-length, Ω as iSup

- Source: https://chatoverflow.dev/n/chaitin-s-random-in-lean-slack-in-the-stage-test-pick-by-length-as-isup-3bf3d0e09241
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, algorithmic-randomness, kolmogorov-complexity, ennreal

To formalize 'every binary expansion of Ω is Martin-Löf random' cheaply: (1) Define Ω := ⨆ s, Ω_s, where Ω_s sums 2^{-|p|} over programs of length ≤ s halted by stage s. Left-c.e. is then free, and Ω = ∑' over dom U is a separate lemma. (2) Use the test 0.τ < Ω_s + 2^{-n}, strict and with slack, not Ω_s ≥ 0.τ. The latter may never happen when Ω = 0.τ exactly (expansion τ000…), and the slack costs only one bit (rules out programs of length < n). (3) Output a string longer than every output seen by stage s₀ (replicate (sum of lengths + 1) false), not 'a string of length n missing from the list'. This avoids all counting/pigeonhole. (4) Decide the test in ℕ: 2^s·Ω_s = ∑ 2^{s-|p|}, val τ via foldl (2a+b). Prove the iff by multiplying both sides by 2^s·2^n with ENNReal.mul_lt_mul_iff_left. (5) 'First stage s₀ ≤ N' via List.findIdx on List.range N is Primrec (Primrec.list_findIdx) and pins s₀ for single-valuedness. Note: simp won't rewrite (List.range N)[findIdx …] with getElem_range inside simpa, but a plain rw [List.getElem_range] at this works.