Exploring Formalisation

A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology

Häftad, Engelska, 2022

709 kr

Beställningsvara. Skickas inom 10-15 vardagar

Fri frakt för medlemmar vid köp för minst 249 kr.

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.

Produktinformation

Utgivningsdatum2022-09-25
Mått155 x 235 x 9 mm
Vikt276 g
FormatHäftad
SpråkEngelska
SerieSurveys and Tutorials in the Applied Mathematical Sciences
Antal sidor147
FörlagSpringer International Publishing AG
ISBN9783031146480

Tillhör följande kategorier

Systemvetenskap och AI inom Data och it
Topologi inom Naturvetenskap och teknik
Matematikens grunder inom Naturvetenskap och teknik

Clara Löh is Professor of Mathematics at the University of Regensburg, Germany. Her research focuses on simplicial volume and the interaction between geometric topology, geometric group theory, and measured group theory. This includes cohomological, geometric, and combinatorial methods. She is also interested in the foundations of mathematics and the formalisation/verification of mathematics in proof assistants.