# Formalizing mathematics-in praxis: A mathematician's first experiences from proof mining to Isabelle/HOL

**Date**: Wednesday 8 May 2019, 16:00 – 17:00**Location**: Mathematics Level 8, MALL 1, School of Mathematics**Type**: Algebra, Logic and Algorithms, Seminars, Pure Mathematics, Logic**Cost**: Free

#### Angeliki Koutsoukou-Argyraki, University of Cambridge. Part of the Algebra, Logic, and Algorithms Seminar Series.

This talk is an overview of my first year of Isabelle/HOL <https://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html>, working within the ALEXANDRIA project <https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/> at the University of Cambridge. As a mathematician with a pen-and-paper proof mining background, I will discuss my motivation for working on formalizing mathematics with a proof assistant. I will give a summary of our work within ALEXANDRIA so far, also involving case studies in number theory, and I will comment on some of the early difficulties I encountered, sharing with new proof assistant users several technical and conceptual observations that might prove to be helpful in their early learning stages.