Title: Verified Optimisation in Lean
Speaker: Ramon Mir Fernandez
Abstract: 
Convex optimisation is a subfield of mathematics that studies convex functions and their maxima/minima over a given domain. It has applications in control synthesis, signal processing and operations research to mention a few. One issue is that reducing these problems to convex optimisation problems is not straightforward and error-prone. Moreover, the approximate nature of the algorithms used by the solvers can make the result unreliable. For these reasons, it would be highly desirable to use a formal tool alongside these solvers to rigorously check every step and certify the final result. We will delve into how the tools can be linked and discuss some work in progress. The formal tool chosen for this project is Lean, a theorem prover and programming language developed at Microsoft Research. We will explain some of its main features and talk about how it differs from other systems such as Coq or Isabelle. Finally, we will explore neural network verification as a potential case study.