Exploring formalisation: a primer in human-readable mathematics in lean 3 with examples from simplicial topology
Auteur :
Löh, Clara
Éditeur :
Springer International Publishing AG
ISBN :
9783031146480
Date de publication :
25 sept. 2022
Dimensions :
23,5 x 15,5 cm
Langue :
Anglais
Pays d'origine :
Suisse
This primer on mathematics formalisation provides a rapid, hands-on introduction to proof verification in Lean. After a quick introduction to Lean, the basic techniques of human-readable formalisation are introduced, illustrated by simple examples on maps, induction and real numbers.