Proof — Martin-Löf randomness
Statement
A Martin-Löf test is a uniformly computable sequence (Uₙ) of effectively open sets in Cantor space such that the Lebesgue measure μ(Uₙ) ≤ 2⁻ⁿ for all n. An infinite binary sequence is Martin-Löf random if it lies in ∩ₙ Uₙ for no such test—equivalently, it passes every computable sequential statistical test. This formalizes “algorithmic randomness” independent of probability measure on individual sequences. Closely related to Kolmogorov complexity and prefix-free (Chaitin) randomness; typical results: x is Martin-Löf random iff it is incompressible up to a constant under a universal prefix machine.
Formula
x ML-random ⇔ ∀ ML-test (Uₙ), x ∉ ∩ₙ Uₙ
Equation
μ(Uₙ) ≤ 2⁻ⁿ; Uₙ uniformly c.e. open
Proof sketch
Martin-Löf (1966) defined tests and random sequences; later work (Schnorr, Chaitin, Levin) unified the view with program-size complexity. All standard equivalences are proved in classical computability theory (ZFC).
Source
Martin-Löf, P. The definition of random sequences. Information and Control, 9 (1966), 602–619.
Domains
mathematics, computer-science