Provedllmlarge-language-modelsformal-proofattention
Attention output in raw exponential form
For all :
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, v1 range over real numbers: the statement must hold for every choice. (
(s0 s1 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, v0, v1. Lean writes f x; papers write f(x). (
TransformerAttention.attend2 s0 s1 v0 v1) - =Equality
- attend2(s0, s1, v0, v1) and exp(s0)/(exp(s0) + exp(s1)) · v0 + exp(s1)/(exp(s0) + exp(… are the same. (
TransformerAttention.attend2 s0 s1 v0 v…) - eˣExponential function
- e raised to the power s0, where e ≈ 2.718. (
Real.exp s0) - a/bDivision
- exp(s0) divided by exp(s0) + exp(s1). In Lean, dividing by 0 gives 0. (
Real.exp s0 / (Real.exp s0 + Real.exp s…) - ·Multiplication
- exp(s0)/(exp(s0) + exp(s1)) times v0. (
Real.exp s0 / (Real.exp s0 + Real.exp s…) - +Addition
- exp(s0) plus exp(s1). (
Real.exp s0 + Real.exp s1)
theorem attn2-attend2-exp-form (s0 s1 v0 v1 : ℝ) :
TransformerAttention.attend2 s0 s1 v0 v1
= Real.exp s0 / (Real.exp s0 + Real.exp s1) * v0
+ Real.exp s1 / (Real.exp s0 + Real.exp s1) * v1attend2 in terms of the two exponentials and values.
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
- 15 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.