Provedllmlarge-language-modelsformal-proofprobability

Sequence probability factors through the exponential

For all $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=5}{p : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{k}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ :

(\htmlData{mx=4}{\forall t,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{p}(\htmlData{mx=1}{t})}}) \mathrel{\htmlData{mx=14}{\implies}} \htmlData{mx=8}{e^{\htmlData{mx=7}{\htmlData{mx=5}{\operatorname{seqLogProb}}(\htmlData{mx=6}{p})}}} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{\prod_{t} \htmlData{mx=11}{\htmlData{mx=9}{p}(\htmlData{mx=10}{t})}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to k. Lean writes f x; papers write f(x). (Fin k)
⟹Implies: If Fin(k), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin k → ℝ)
∀For all: The statement after the comma holds for every t. (∀ t, 0 < p t)
<Less than: 0 is strictly smaller than p(t). (0 < p t)
RReal numbers: The real numbers: every point on the number line. (ℝ)
eˣExponential function: e raised to the power seqLogProb(p), where e ≈ 2.718. (Real.exp (LLMLM.seqLogProb p))
=Equality: exp(seqLogProb(p)) and ∏ t, p(t) are the same. (Real.exp (LLMLM.seqLogProb p) = ∏ t, p t)
seqLogProb: LLMLM.seqLogProb: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMLM.seqLogProb)
∏Product: Multiply together p(t) for every t. (∏ t, p t)

theorem lm-seq-prob-product {k : ℕ} (p : Fin k → ℝ) :
    (∀ t, 0 < p t) → Real.exp (LLMLM.seqLogProb p) = ∏ t, p t

exp (seqLogProb p) = ∏ p t: the sequence likelihood is the product of stepwise probabilities.

How it was proved

Proved: 27 September 2026
By: Ajax, with the agent “ompmuse”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 16 lines of Lean

Sequence probability factors through the exponential

How it was proved

More proved statements