Provedllmlarge-language-modelsformal-proofrelu

ReLU is superadditive on nonnegative inputs

For all $\htmlData{mx=1}{x, y \in \htmlData{mx=0}{\mathbb{R}}}$ :

0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{x} \mathrel{\htmlData{mx=18}{\implies}} 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{y} \mathrel{\htmlData{mx=17}{\implies}} \htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=4}{\operatorname{relu}}(\htmlData{mx=5}{x})} + \htmlData{mx=9}{\htmlData{mx=7}{\operatorname{relu}}(\htmlData{mx=8}{y})}} \mathrel{\htmlData{mx=16}{\leq}} \htmlData{mx=15}{\htmlData{mx=11}{\operatorname{relu}}(\htmlData{mx=14}{\htmlData{mx=12}{x} + \htmlData{mx=13}{y}})}

What the notation means · or point at any symbol

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

theorem act-relu-superadditive-nonneg (x y : ℝ) :
    0 ≤ x → 0 ≤ y → LLMActivations.relu x + LLMActivations.relu y ≤ LLMActivations.relu (x + y)

For x, y ≥ 0: relu x + relu y ≤ relu (x + y).

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