Angeliki Koutsoukou-Argyraki (Oct 13 2020 at 07:34): Angeliki Koutsoukou-Argyraki (Oct 13 2020 at 07:34):My review article on my first Isabelle experiences has appeared on the Jahresbericht der Deutschen Mathematiker-Vereinigung (Springer)
Open Access pdf:
https://link.springer.com/article/10.1365/s13291-020-00221-1
May be of interest for students, mathematicians interested to enter the world of formalisation.
Includes discussions on my first projects and on the rationale behind formalising mathematics and the choice of Isabelle/HOL in particular, some basic instructions for new users, some technical and conceptual observations focussing on some of the first difficulties encountered, and some thoughts on the use and potential of proof assistants for mathematics.
Last updated: Dec 22 2024 at 04:21 UTC