Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Koutsoukou-Argyraki, A
Abstract
jats:titleAbstract</jats:title>jats:pThis is an account of a mathematician’s first experiences with the proof assistant (interactive theorem prover) Isabelle/HOL, including a discussion on the rationale behind formalising mathematics and the choice of Isabelle/HOL in particular, some 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.</jats:p>
Description
Keywords
4904 Pure Mathematics, 49 Mathematical Sciences
Journal Title
Jahresbericht der Deutschen Mathematiker-Vereinigung
Conference Name
Journal ISSN
0012-0456
1869-7135
1869-7135
Volume Title
123
Publisher
Springer Fachmedien Wiesbaden GmbH
Publisher DOI
Sponsorship
European Research Council (742178)