Formal foundations

mononet’s constrained-monotonic construction rests on results with machine-checked proofs. The formalization — Lean 4 + mathlib4, sorry-free — lives in the companion repository neural-network-proofs.

It mechanizes the universal-approximation lineage behind the method: Cybenko (1989), Leshno–Lin–Pinkus–Schocken (1993), Mikulincer–Reichman (2022), Sartor et al. (2025), the deep constrained-monotonic result (Runje et al.), and Amos et al. (2017) input-convex networks.

Browse the proofs, the interactive blueprint (proof sketches + dependency graph), and the doc-gen4 API reference at the project’s rendered docs:

• Docs & blueprint: https://davorrunje.github.io/neural-network-proofs/

• Source: davorrunje/neural-network-proofs