Provedalphabaguetteattentionnumerics
Base-two exponent with a folded log₂e scale computes eˣ: 2^(x/ln 2) = exp x
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - (x : T)As real numbers
- 2 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(2:ℝ)) - aᵇPower
- 2 raised to the power x · (1/log(2)). (
(2:ℝ) ^ (x * (1 / Real.log 2))) - =Equality
- 2^(x · (1/log(2))) and exp(x) are the same. (
(2:ℝ) ^ (x * (1 / Real.log 2)) = Real.e…) - ·Multiplication
- x times 1/log(2). (
x * (1 / Real.log 2)) - a/bDivision
- 1 divided by log(2). In Lean, dividing by 0 gives 0. (
1 / Real.log 2) - logNatural logarithm
- The logarithm of 2 to base e: the power e must be raised to to give 2. (
Real.log 2) - eˣExponential function
- e raised to the power x, where e ≈ 2.718. (
Real.exp x)
theorem exp2-log2e-scale-is-exp (x : ℝ) :
(2:ℝ) ^ (x * (1 / Real.log 2)) = Real.exp xBaguette's kernels use only the hardware exp2. The sigmoid gate multiplies by log₂e before exp2 (sigmoidFromExp2With), and attention folds log₂e into its score scale (baguetteAttentionBaseTwoScaleWord = 1/(√64 · ln 2), Alpha commit e3330947, systems/baguette/src/Baguette/Model.alpha). Over ℝ this is exact: 2^(x · (1/ln 2)) = eˣ. The softmax and sigmoid they compute are therefore the natural-base ones; only rounding differs.
How it was proved
- Proved
- 3 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- 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.