Abstract: 

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.