Provedcommons

Softmax over two logits is the sigmoid of their difference

For all $\htmlData{mx=4}{x : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Fin}}\,2} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{softmax}}(\htmlData{mx=1}{x}, 0)} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=3}{\operatorname{sigmoid}}(\htmlData{mx=8}{\htmlData{mx=5}{\htmlData{mx=4}{x}(0)} - \htmlData{mx=7}{\htmlData{mx=6}{x}(1)}})}

What the notation means · or point at any symbol

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 2. Lean writes f x; papers write f(x). (Fin 2)
⟹Implies: If Fin(2), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin 2 → ℝ)
softmax: Commons.softmax: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.softmax)
=Equality: softmax(x, 0) and sigmoid(x(0) − x(1)) are the same. (Commons.softmax x 0 = Real.sigmoid (x 0…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
sigmoid: Real.sigmoid: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Real.sigmoid)
-Subtraction: x(0) minus x(1). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (x 0 - x 1)

theorem softmax-two-is-sigmoid (x : Fin 2 → ℝ) :
    Commons.softmax x 0 = Real.sigmoid (x 0 - x 1)

From our commons: Commons.softmax_fin_two in the Commons.ML.Softmax definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
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: 9 lines of Lean