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

Dr 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, working within the ALEXANDRIA project 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.