proofs
Provedllmlarge-language-modelsformal-proofattention

Attention is homogeneous in the pair of values

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

attend2⁡(s0,s1,c⋅v0,c⋅v1)=c⋅attend2⁡(s0,s1,v0,v1)\htmlData{mx=9}{\htmlData{mx=0}{\operatorname{attend2}}(\htmlData{mx=1}{s_{0}}, \htmlData{mx=2}{s_{1}}, \htmlData{mx=5}{\htmlData{mx=3}{c} \cdot \htmlData{mx=4}{v_{0}}}, \htmlData{mx=8}{\htmlData{mx=6}{c} \cdot \htmlData{mx=7}{v_{1}}})} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\htmlData{mx=10}{c} \cdot \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}})}}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
s0, s1, c, v0, v1 range over real numbers: the statement must hold for every choice. ((s0 s1 c v0 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, c · v0, c · v1. Lean writes f x; papers write f(x). (TransformerAttention.attend2 s0 s1 (c *…)
=Equality
attend2(s0, s1, c · v0, c · v1) and c · attend2(s0, s1, v0, v1) are the same. (TransformerAttention.attend2 s0 s1 (c *…)
·Multiplication
c times v0. (c * v0)

Scaling both values scales the attention output by the same factor.

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

More proved statements