Email Gateway (Jun 26 2025 at 13:27): Email Gateway (Jun 26 2025 at 13:27):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry:
The Sigmoid Function and the Universal Approximation Theorem
by Dustin Bryant, Jim Woodcock and Simon Foster
We present a machine-checked Isabelle/HOL development of the sigmoid function
sigma(x) = e^x / (1 + e^x)
together with its most important analytic properties. After proving positivity,
strict monotonicity, C^infinity smoothness, and the limits at plus/minus
infinity, we derive a closed-form expression for the n-th derivative using
Stirling numbers of the second kind, following the combinatorial argument of
Minai and Williams. These results are packaged into a small reusable library of
lemmas on sigma. Building on this analytic groundwork we mechanise a
constructive version of the classical Universal Approximation Theorem: for every
continuous function f : [a,b] -> R and every epsilon > 0 there is a
single‑hidden‑layer neural network with sigmoidal activations whose output is
within epsilon of f everywhere on [a,b]. Our proof follows the method of
Costarell and Spigler, giving the first fully verified end-to‑end proof of this
theorem inside a higher‑order proof assistant.
https://www.isa-afp.org/entries/Sigmoid_Universal_Approximation.html
Enjoy,
René
Last updated: Jul 02 2025 at 04:31 UTC