Provedllmlarge-language-modelsformal-proofsigmoid

Sigmoid plus its complement form

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

\htmlData{mx=7}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{sigmoid}}(\htmlData{mx=1}{x})} + \htmlData{mx=6}{\htmlData{mx=3}{\operatorname{sigmoid}}(\htmlData{mx=5}{-\htmlData{mx=4}{x}})}} \mathrel{\htmlData{mx=8}{=}} 1

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
sigmoid: LLMActivations.sigmoid: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (LLMActivations.sigmoid)
f(x)Function application: LLMActivations.sigmoid applied to x. Lean writes f x; papers write f(x). (LLMActivations.sigmoid x)
+Addition: sigmoid(x) plus sigmoid(−x). (LLMActivations.sigmoid x + LLMActivatio…)
=Equality: sigmoid(x) + sigmoid(−x) and 1 are the same. (LLMActivations.sigmoid x + LLMActivatio…)
−xNegation: The negative of x. (-x)

theorem act-sigmoid-sum-complement (x : ℝ) :
    LLMActivations.sigmoid x + LLMActivations.sigmoid (-x) = 1

σ(x) + σ(−x) = 1 restated as σ(−x) = 1 − σ(x) sum form.

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