Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started

Thumbnail
View / Open Files
Authors
Koutsoukou-Argyraki, Angeliki
Publication Date
2020-10-06
Journal Title
Jahresbericht der Deutschen Mathematiker-Vereinigung
ISSN
0012-0456
Publisher
Springer Berlin Heidelberg
Volume
123
Issue
1
Pages
3-26
Language
en
Type
Article
This Version
VoR
Metadata
Show full item record
Citation
Koutsoukou-Argyraki, A. (2020). Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started. Jahresbericht der Deutschen Mathematiker-Vereinigung, 123 (1), 3-26. https://doi.org/10.1365/s13291-020-00221-1
Abstract
Abstract: This 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.
Keywords
Survey Article, Interactive theorem proving, Isabelle/HOL, Proof assistant, Formalisation of mathematics, 03B35, 68V15, 68V20, 68V35
Identifiers
s13291-020-00221-1, 221
External DOI: https://doi.org/10.1365/s13291-020-00221-1
This record's URL: https://www.repository.cam.ac.uk/handle/1810/316551

Rights
Attribution 4.0 International (CC BY 4.0)
Licence URL: https://creativecommons.org/licenses/by/4.0/

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)