proofs
Provedattentiontransformersoftmaxformal-proof

Two-key attention output lies between its scalar values

For all s0,s1,v0,v1∈R\htmlData{mx=1}{s_{0}, s_{1}, v_{0}, v_{1} \in \htmlData{mx=0}{\mathbb{R}}}, if v0≤v1\htmlData{mx=0}{v_{0}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{v_{1}}, then

v0≤attend2⁡(s0,s1,v0,v1)∧attend2⁡(s0,s1,v0,v1)≤v1\htmlData{mx=0}{v_{0}} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\htmlData{mx=1}{\operatorname{attend2}}(\htmlData{mx=2}{s_{0}}, \htmlData{mx=3}{s_{1}}, \htmlData{mx=4}{v_{0}}, \htmlData{mx=5}{v_{1}})} \mathbin{\htmlData{mx=16}{\land}} \htmlData{mx=13}{\htmlData{mx=8}{\operatorname{attend2}}(\htmlData{mx=9}{s_{0}}, \htmlData{mx=10}{s_{1}}, \htmlData{mx=11}{v_{0}}, \htmlData{mx=12}{v_{1}})} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{v_{1}}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
s₀, s₁, v₀, v₁ range over real numbers: the statement must hold for every choice. ((s₀ s₁ v₀ v₁ : ℝ))
≤At most
v₀ is less than or equal to v₁. (v₀ ≤ v₁)
∧And
Both hold: v₀ ≤ attend2(s₀, s₁, v₀, v₁), and attend2(s₀, s₁, v₀, v₁) ≤ v₁. (v₀ ≤ attend2 s₀ s₁ v₀ v₁ ∧ attend2 s₀ s…)
attend2
attend2: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (attend2)
f(x)Function application
attend2 applied to s₀, s₁, v₀, v₁. Lean writes f x; papers write f(x). (attend2 s₀ s₁ v₀ v₁)

A property of one-query, two-key scaled dot-product attention with scalar values; scores already include the dot-product scale.

How it was proved

Proved
26 September 2026
By
Ajax, with the agent “Codex attention proofs 2026-09-26”
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
35 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements