Provedalphabaguetteswiglubackward
SwiGLU gate: Alpha's slope σ(x)(1 + x(1 − σ(x))) is the derivative of x·σ(x)
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - HasDerivAt
- HasDerivAt: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
HasDerivAt) - f(x)Function application
- HasDerivAt applied to y ↦ y · (1 + exp(−y))⁻¹, (1 + exp(−x))⁻¹ · (1 + x · (1 − (1 + exp(−x))⁻¹)), x. Lean writes f x; papers write f(x). (
HasDerivAt (fun y : ℝ => y * (1 + Real.…) - x ↦ f(x)Function (λ-abstraction)
- The function sending y to y · (1 + exp(−y))⁻¹. Lean writes fun x => …; papers write x ↦ …. (
fun y : ℝ => y * (1 + Real.exp (-y))⁻¹) - ·Multiplication
- y times (1 + exp(−y))⁻¹. (
y * (1 + Real.exp (-y))⁻¹) - x⁻¹Inverse
- The inverse of 1 + exp(−y): what undoes it (1/x for numbers). (
(1 + Real.exp (-y))⁻¹) - +Addition
- 1 plus exp(−y). (
1 + Real.exp (-y)) - eˣExponential function
- e raised to the power −y, where e ≈ 2.718. (
Real.exp (-y)) - −xNegation
- The negative of y. (
-y) - -Subtraction
- 1 minus (1 + exp(−x))⁻¹. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - (1 + Real.exp (-x))⁻¹)
theorem silu-slope-is-derivative (x : ℝ) :
HasDerivAt (fun y : ℝ => y * (1 + Real.exp (-y))⁻¹) ((1 + Real.exp (-x))⁻¹ * (1 + x * (1 - (1 + Real.exp (-x))⁻¹))) xBaguette's feed-forward is h = up · x·σ(x) with σ(x) = (1 + e^(−x))⁻¹ (Component.SigmoidWeightedGate, used through baguetteGatedFeedForwardWith). propagateSigmoidWeightedGateWith multiplies the upstream cotangent by σ(x)·(1 + x·(1 − σ(x))). This proves that slope is the true derivative of x·σ(x) over ℝ.
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
- 20 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.