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.