Provedllmlarge-language-modelsformal-proofscaling-law

The fitted loss stays above the irreducible loss

For all $\htmlData{mx=1}{c, a, \alpha, N \in \htmlData{mx=0}{\mathbb{R}}}$ :

0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{N} \mathrel{\htmlData{mx=16}{\implies}} 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{a} \mathrel{\htmlData{mx=15}{\implies}} 0 \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\alpha} \mathrel{\htmlData{mx=14}{\implies}} \htmlData{mx=6}{c} \mathrel{\htmlData{mx=13}{<}} \htmlData{mx=12}{\htmlData{mx=7}{\operatorname{law}}(\htmlData{mx=8}{c}, \htmlData{mx=9}{a}, \htmlData{mx=10}{\alpha}, \htmlData{mx=11}{N})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: c, a, α, N range over real numbers: the statement must hold for every choice. ((c a α N : ℝ))
<Less than: 0 is strictly smaller than N. (0 < N)
≤At most: 0 is less than or equal to α. (0 ≤ α)
⟹Implies: If 0 ≤ α, then c < law(c, a, α, N). (Between types, A → B is the type of functions from A to B.) (0 ≤ α → c < LLMScaling.law c a α N)
law: LLMScaling.law: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMScaling.law)
f(x)Function application: LLMScaling.law applied to c, a, α, N. Lean writes f x; papers write f(x). (LLMScaling.law c a α N)

theorem scaling-above-floor (c a α N : ℝ) :
    0 < N → 0 < a → 0 ≤ α → c < LLMScaling.law c a α N

For a > 0 the reducible term is positive, so L(N) > c.

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: 17 lines of Lean