Thursday, 6th of October 2022, 12:00 – 1:00

Formalising Mathematics in Isabelle/HOL


Manuel Eberl - researcher at CL


In this talk, I give a very high-level overview about some recent work concerning the formalisation of mathematics in the interactive theorem prover Isabelle/HOL. I start with a very brief look at what Isabelle/HOL is and what formalised mathematics looks like. Then I show two particular problems that I encountered and how I solved them, namely asymptotic estimates of real-valued functions and complicated integration contours arising in Analytic Number Theory.


Nach oben scrollen