In this project, you will formalize artificial neural networks in the interactive proof assistant Isabelle. Isabelle is a software tool that allows the user to build formal models using a precise language with clear (formal) semantics. This language offers both concepts from programming (e.g., datatypes, recursive functions) and mathematical concepts (e.g., real numbers, quantifiers).
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.