This project is a formalization of the 1993 Leshno et al. proof of the Universal Approximation Theorem for neural networks. Along the way I am also proving various useful theorems in approximation theory used in the paper, so I will try to separate those from the UAT proof so they can be used on their own as well. Currently a work in progress, just finished a minimum working proof of Step 1 and I'm now on to cleaning it up and doing Step 2.