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
Dr Angeliki Koutsoukou-Argyraki, University of Cambridge. Part of the Algebra, Logic, and Algorithms Seminar Series.
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.