proofs
Provedllmlarge-language-modelsformal-proofattention

Attention is additive in the pair of values

For all s0,s1,v0,v0′,v1,v1′∈R\htmlData{mx=1}{s_{0}, s_{1}, v_{0}, v_{0}', v_{1}, v_{1}' \in \htmlData{mx=0}{\mathbb{R}}}:

attend2⁡(s0,s1,v0+v0′,v1+v1′)=attend2⁡(s0,s1,v0,v1)+attend2⁡(s0,s1,v0′,v1′)\begin{aligned} & \htmlData{mx=10}{\htmlData{mx=1}{\operatorname{attend2}}(\htmlData{mx=2}{s_{0}}, \htmlData{mx=3}{s_{1}}, \htmlData{mx=6}{\htmlData{mx=4}{v_{0}} + \htmlData{mx=5}{v_{0}'}}, \htmlData{mx=9}{\htmlData{mx=7}{v_{1}} + \htmlData{mx=8}{v_{1}'}})} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=23}{\htmlData{mx=16}{\htmlData{mx=11}{\operatorname{attend2}}(\htmlData{mx=12}{s_{0}}, \htmlData{mx=13}{s_{1}}, \htmlData{mx=14}{v_{0}}, \htmlData{mx=15}{v_{1}})} + \htmlData{mx=22}{\htmlData{mx=17}{\operatorname{attend2}}(\htmlData{mx=18}{s_{0}}, \htmlData{mx=19}{s_{1}}, \htmlData{mx=20}{v_{0}'}, \htmlData{mx=21}{v_{1}'})}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
s0, s1, v0, v0', v1, v1' range over real numbers: the statement must hold for every choice. ((s0 s1 v0 v0' v1 v1' : ℝ))
attend2
TransformerAttention.attend2: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (TransformerAttention.attend2)
f(x)Function application
TransformerAttention.attend2 applied to s0, s1, v0 + v0', v1 + v1'. Lean writes f x; papers write f(x). (TransformerAttention.attend2 s0 s1 (v0 …)
=Equality
attend2(s0, s1, v0 + v0', v1 + v1') and attend2(s0, s1, v0, v1) + attend2(s0, s1, v0', v1') are the same. (TransformerAttention.attend2 s0 s1 (v0 …)
+Addition
v0 plus v0'. (v0 + v0')

attend2 of the pointwise sum equals the sum of the attend2 outputs.

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
14 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements