Random typing produces a power law in rank (Li's model)

Proved

ZipfLaw.monkey_typing_power_law

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

harmonic-numberspower-lawzipf-law

Consider a monkey typing on a keyboard with $m\ge2$ letter keys, each pressed with the same probability $q>0$ , and a space bar pressed with probability $1-mq>0$ . The probability that the word following a space is exactly the string $w$ of letters is $p(w)=q^{|w|}(1-mq)$ . List all nonempty words in order of non-increasing probability, $w_1,w_2,w_3,\dots$ (ties in any order). Then the probability of the word of rank $r$ obeys a power law in $r$ : with $\alpha=\log_m(1/q)$ there are constants $0<C_1\le C_2$ such that for all $r\ge1$

C_1\,r^{-\alpha}\le p(w_r)\le C_2\,r^{-\alpha}.

Formalization Note. Ranks are $0$ -indexed in Lean: the rank order is a bijection $e:\mathbb N\to\{\text{nonempty words}\}$ along which $p$ is non-increasing, and the bound is stated with $(r+1)^{-\alpha}$ .

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem monkey_typing_power_law (m : ℕ) (hm : 2 ≤ m) (q : ℝ) (hq : 0 < q) (hmq : (m : ℝ) * q < 1)
    (e : ℕ → List (Fin m)) (he_inj : Function.Injective e)
    (he_range : Set.range e = {w | w ≠ []})
    (he_sorted : Antitone (fun r => monkeyWordProb m q (e r))) :
    ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧ ∀ r : ℕ,
      C₁ * ((r : ℝ) + 1) ^ (-Real.logb m (1 / q)) ≤ monkeyWordProb m q (e r) ∧
        monkeyWordProb m q (e r) ≤ C₂ * ((r : ℝ) + 1) ^ (-Real.logb m (1 / q)) := by sorry

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, section "Statistical explanations" (Li: "in a document in which each character has been chosen randomly from a uniform distribution of all letters (plus a space character), the 'words' with different lengths follow the macro-trend of Zipf's law"; ref. Li 1992, https://doi.org/10.1109/18.165464).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent reader, and no reviewer should treat it as one. Please compare it against the Lean code yourself.

Let $m\ge2$ be a natural number, $q$ a real with $q>0$ and $mq<1$ . Let $e$ be a function from $\mathbb N$ to finite lists over an $m$ -letter alphabet which is injective, whose image is exactly the set of nonempty lists, and such that $r\mapsto q^{|e(r)|}(1-mq)$ is antitone (non-increasing in $r$ ). Then there exist reals $C_1>0$ and $C_2>0$ such that for every natural $r$ :

C_1\,(r+1)^{-\log_m(1/q)}\le q^{|e(r)|}(1-mq)\le C_2\,(r+1)^{-\log_m(1/q)},

with $\log_m(1/q)=\ln(1/q)/\ln m$ and real powers.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph