Provedllmlarge-language-modelsformal-proofsigmoid

Sigmoid odds are positive and exponential

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

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

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
<Less than: 0 is strictly smaller than sigmoid(x)/(1 − sigmoid(x)). (0 < LLMActivations.sigmoid x / (1 - LLM…)
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)
a/bDivision: sigmoid(x) divided by 1 − sigmoid(x). In Lean, dividing by 0 gives 0. (LLMActivations.sigmoid x / (1 - LLMActi…)
-Subtraction: 1 minus sigmoid(x). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - LLMActivations.sigmoid x)

theorem act-sigmoid-odds-pos (x : ℝ) :
    0 < LLMActivations.sigmoid x / (1 - LLMActivations.sigmoid x)

For all x: sigmoid x / (1 − sigmoid x) > 0 (strict form of the odds identity).

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