Provedllmlarge-language-modelsformal-proofsoftmax

Softmax over one token 1 concentrates fully

\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{sm}}(\htmlData{mx=3}{\cdot \mapsto 1}, 0)} \mathrel{\htmlData{mx=5}{=}} 1

What the notation means · or point at any symbol

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)
=Equality: sm(_ ↦ 1, 0) and 1 are the same. (LLMSoftmax.sm (fun _ : Fin 1 => 1) 0 = 1)
x ↦ f(x)Function (λ-abstraction): The function sending _ to 1. Lean writes fun x => …; papers write x ↦ …. (fun _ : Fin 1 => 1)
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 1. Lean writes f x; papers write f(x). (Fin 1)

theorem smx-single-one :
    LLMSoftmax.sm (fun _ : Fin 1 => 1) 0 = 1

sm (fun _ : Fin 1 => 1) 0 = 1.

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