Universal approximation theorems, formalized in Lean 4 + Mathlib.
All results are sorry-free and axiom-clean (propext, Classical.choice, Quot.sound)A single-hidden-layer network with a continuous sigmoidal activation is dense in C(K, ℝ).
An M-class activation densely approximates iff it is not (almost everywhere) a polynomial.
A depth-4 monotone threshold network exactly interpolates, and uniformly approximates, any monotone function.
Monotone networks with one-sided-saturating activations are universal — extending beyond bounded activations, via non-negative alternating-saturation or (equivalently) non-positive weights.
Deep Constrained Monotonic Neural Networks: skip connections make deep constrained monotone networks trainable — formalized soundness (a residual stack of any depth is monotone) and universal approximation, with partial monotonicity as a secondary result.
Extends Runje–Shankaranarayana 2023.
Input-Convex Neural Networks: ICNN soundness and convex universal approximation formalized — fully input-convex networks denote convex functions of their input, and any convex, differentiable function is uniformly approximated on any compact set by such a network; the general non-differentiable case is forthcoming.