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

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.