Provedllmlarge-language-modelsformal-prooflog-likelihood

seqLogProb in named form

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=2}{\htmlData{mx=0}{\operatorname{seqLogProb}}(\htmlData{mx=1}{p})} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\sum_{t} \htmlData{mx=6}{\log \htmlData{mx=5}{\htmlData{mx=3}{p}(\htmlData{mx=4}{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 → ℝ)
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)
=Equality: seqLogProb(p) and ∑ t, log(p(t)) are the same. (LLMLM.seqLogProb p = ∑ t, Real.log (p t))
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up log(p(t)) for every t. (∑ t, Real.log (p t))
logNatural logarithm: The logarithm of p(t) to base e: the power e must be raised to to give p(t). (Real.log (p t))

theorem lm-seqlog-def {k : ℕ} (p : Fin k → ℝ) :
    LLMLM.seqLogProb p = ∑ t, Real.log (p t)

LLMLM.seqLogProb p = ∑ t, Real.log (p t).

How it was proved

Proved: 28 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: 14 lines of Lean

seqLogProb in named form

How it was proved

More proved statements