Provedllmlarge-language-modelsformal-prooflayernorm
mean in named form
For all and :
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - mean
- LLMLayerNorm.mean: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
LLMLayerNorm.mean) - =Equality
- mean(x) and (∑ i, x(i))/n are the same. (
LLMLayerNorm.mean x = (∑ i, x i) / (n :…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - a/bDivision
- ∑ i, x(i) divided by n. In Lean, dividing by 0 gives 0. (
(∑ i, x i) / (n : ℝ)) - ∑Summation
- Add up x(i) for every i. (
∑ i, x i) - (x : T)As real numbers
- n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(n : ℝ))
theorem ln-mean-def {n : ℕ} (x : Fin n → ℝ) :
LLMLayerNorm.mean x = (∑ i, x i) / (n : ℝ)LLMLayerNorm.mean x = (∑ i, x i) / (n : ℝ).
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
- 13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.