Provedllmlarge-language-modelsformal-proofrelu
ReLU at one
What the notation means · or point at any symbol
- 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 1. Lean writes f x; papers write f(x). (
LLMActivations.relu 1) - =Equality
- relu(1) and 1 are the same. (
LLMActivations.relu 1 = 1)
theorem act-relu-one :
LLMActivations.relu 1 = 1relu 1 = 1.
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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.