Neural Network Universal Approximation — Blueprint

1 Introduction

This blueprint presents the formalized universal approximation theorems (UATs) for neural networks developed in Lean 4 and Mathlib, across six developments. Each result is stated informally, accompanied by its formal Lean statement and a prose proof, and is cross-linked to the formal API. Every item marked green is fully formalized and sorry-free.

  • Cybenko (1989): a single-hidden-layer network with a continuous sigmoidal activation is dense in \(C(K,\mathbb {R})\).

  • Leshno–Lin–Pinkus–Schocken (1993): an \(M\)-class activation densely approximates iff it is not (a.e.) a polynomial.

  • Mikulincer–Reichman (2022): depth-4 monotone threshold networks exactly interpolate and uniformly approximate any monotone function.

  • Sartor et al. (2025): monotone one-sided-saturating activations are universal, extending beyond bounded activations.

  • Runje et al. (forthcoming): Deep Constrained Monotonic Neural Networks — skip connections make deep constrained monotone networks trainable, with formalized soundness (a residual stack of any depth is monotone) and universal approximation; partial monotonicity is a secondary result. Extends Runje–Shankaranarayana 2023.

  • Amos–Xu–Kolter (2017): Input-Convex Neural Networks — fully input-convex networks (FICNNs) denote convex functions of their input; ICNN soundness and universal approximation (for differentiable convex functions) are formalized, with the general non-differentiable case forthcoming.

The three monotone developments (Mikulincer–Reichman, Sartor, Runje) share a common, activation-generic ActStack core.