Provedllmlarge-language-modelsformal-proofsoftmax

Softmax respects pointwise equality of logits

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

(\htmlData{mx=7}{\forall j,\ \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{j})} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\htmlData{mx=3}{w'}(\htmlData{mx=4}{j})}}) \mathrel{\htmlData{mx=17}{\implies}} \htmlData{mx=11}{\htmlData{mx=8}{\operatorname{sm}}(\htmlData{mx=9}{w}, \htmlData{mx=10}{i})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=12}{\operatorname{sm}}(\htmlData{mx=13}{w'}, \htmlData{mx=14}{i})}

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 n. Lean writes f x; papers write f(x). (Fin n)
⟹Implies: If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℝ)
x : TVariables: w, w' range over Fin n → ℝ: the statement must hold for every choice. ((w w' : Fin n → ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, w j = w' j)
=Equality: w(j) and w'(j) are the same. (w j = w' j)
RReal numbers: The real numbers: every point on the number line. (ℝ)
sm: LLMSoftmax.sm: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMSoftmax.sm)

theorem smx-congr (n : ℕ) (w w' : Fin n → ℝ) (i : Fin n) :
    (∀ j, w j = w' j) → LLMSoftmax.sm w i = LLMSoftmax.sm w' i

If w and w' agree everywhere, their softmax weights agree.

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: 18 lines of Lean

Softmax respects pointwise equality of logits

How it was proved

More proved statements