國立高雄大學圖資館 |

Language: English

Back

Exploring formalisationa primer in human-readable mathematics in Lean 3 with examples from simplicial topology /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Exploring formalisationby Clara Loh.
Reminder of title:	a primer in human-readable mathematics in Lean 3 with examples from simplicial topology /
Author:	Loh, Clara.
Published:	Cham :Springer International Publishing :2022.
Description:	vi, 147 p. :ill., digital ;24 cm.
Contained By:	Springer Nature eBook
Subject:	Automatic theorem provingComputer programs.
Online resource:	https://doi.org/10.1007/978-3-031-14649-7
ISBN:	9783031146497$q(electronic bk.)

Exploring formalisationa primer in human-readable mathematics in Lean 3 with examples from simplicial topology /
Loh, Clara.

Exploring formalisationa primer in human-readable mathematics in Lean 3 with examples from simplicial topology /[electronic resource] :by Clara Loh. - Cham :Springer International Publishing :2022. - vi, 147 p. :ill., digital ;24 cm. - Surveys and tutorials in the applied mathematical sciences,v. 112199-4773 ;. - Surveys and tutorials in the applied mathematical sciences ;v.7..

Introduction -- 1 The Lean Proof Assistant -- 2 Basic Examples -- 3 Design Choices -- 4 Abstraction and Prototyping.

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. Subsequently, typical design options are discussed and brought to life through worked examples in the setting of simplicial complexes (a higher-dimensional generalisation of graph theory) Finally, the book demonstrates how current research in algebraic and geometric topology can be formalised by means of suitable abstraction layers. Informed by the author's recent teaching and research experience, this book allows students and researchers to quickly get started with formalising and checking their proofs. The core material of the book is accessible to mathematics students with basic programming skills. For the final chapter, familiarity with elementary category theory and algebraic topology is recommended.

ISBN: 9783031146497$q(electronic bk.)

Standard No.: 10.1007/978-3-031-14649-7doiSubjects--Topical Terms:

936022
Automatic theorem proving
--Computer programs.

LC Class. No.: QA76.9.A96 / L2 2022

Dewey Class. No.: 511.3

Exploring formalisationa primer in human-readable mathematics in Lean 3 with examples from simplicial topology /
LDR:02307nmm a2200361 a 4500 001 630689
003 DE-He213
005 20220924152834.0
006 m d
007 cr nn 008maaau
008 230329s2022 sz s 0 eng d
020 $a 9783031146497$q(electronic bk.)
020 $a 9783031146480$q(paper)
024 7 $a 10.1007/978-3-031-14649-7 $2 doi
035 $a 978-3-031-14649-7
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.A96 $b L2 2022
072 7 $a PBCD $2 bicssc
072 7 $a PBC $2 bicssc
072 7 $a MAT018000 $2 bisacsh
072 7 $a PBCD $2 thema
072 7 $a PBC $2 thema
082 0 4 $a 511.3 $2 23
090 $a QA76.9.A96 $b L833 2022
100 1 $a Loh, Clara. $3 798198
245 1 0 $a Exploring formalisation $h [electronic resource] : $b a primer in human-readable mathematics in Lean 3 with examples from simplicial topology / $c by Clara Loh.
260 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2022.
300 $a vi, 147 p. : $b ill., digital ; $c 24 cm.
490 1 $a Surveys and tutorials in the applied mathematical sciences, $x 2199-4773 ; $v v. 11
505 0 $a Introduction -- 1 The Lean Proof Assistant -- 2 Basic Examples -- 3 Design Choices -- 4 Abstraction and Prototyping.
520 $a 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. Subsequently, typical design options are discussed and brought to life through worked examples in the setting of simplicial complexes (a higher-dimensional generalisation of graph theory) Finally, the book demonstrates how current research in algebraic and geometric topology can be formalised by means of suitable abstraction layers. Informed by the author's recent teaching and research experience, this book allows students and researchers to quickly get started with formalising and checking their proofs. The core material of the book is accessible to mathematics students with basic programming skills. For the final chapter, familiarity with elementary category theory and algebraic topology is recommended.
650 0 $a Automatic theorem proving $x Computer programs. $3 936022
650 1 4 $a Mathematical Logic and Foundations. $3 274479
650 2 4 $a Algebraic Topology. $3 273784
650 2 4 $a Formal Languages and Automata Theory. $3 914922
650 2 4 $a Symbolic and Algebraic Manipulation. $3 273720
650 2 4 $a Manifolds and Cell Complexes. $3 913127
710 2 $a SpringerLink (Online service) $3 273601
773 0 $t Springer Nature eBook
830 0 $a Surveys and tutorials in the applied mathematical sciences ; $v v.7. $3 860019
856 4 0 $u https://doi.org/10.1007/978-3-031-14649-7
950 $a Mathematics and Statistics (SpringerNature-11649)