國立虎尾科技大學 |

Exploring Formalisation = A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Exploring Formalisation/ by Clara Löh.
其他題名:	A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /
作者:	Löh, Clara.
面頁冊數:	VI, 147 p. 1 illus.online resource. :
Contained By:	Springer Nature eBook
標題:	Manifolds and Cell Complexes. -
電子資源:	https://doi.org/10.1007/978-3-031-14649-7
ISBN:	9783031146497

Exploring Formalisation = A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /
Löh, Clara.

Exploring FormalisationA Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /[electronic resource] :by Clara Löh. - 1st ed. 2022. - VI, 147 p. 1 illus.online resource. - Surveys and Tutorials in the Applied Mathematical Sciences,112199-4773 ;. - Surveys and Tutorials in the Applied Mathematical Sciences,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

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

1366170
Manifolds and Cell Complexes.

LC Class. No.: QA8.9-10.3

Dewey Class. No.: 511.3

Exploring Formalisation = A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /
LDR:02614nam a22004215i 4500 001 1083546
003 DE-He213
005 20220924152834.0
007 cr nn 008mamaa
008 221228s2022 sz | s |||| 0|eng d
020 $a 9783031146497 $9 978-3-031-14649-7
024 7 $a 10.1007/978-3-031-14649-7 $2 doi
035 $a 978-3-031-14649-7
050 4 $a QA8.9-10.3
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
100 1 $a Löh, Clara. $e editor. $4 aut $4 http://id.loc.gov/vocabulary/relators/aut $3 1274652
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 Löh.
250 $a 1st ed. 2022.
264 1 $a Cham : $b Springer International Publishing : $b Imprint: Springer, $c 2022.
300 $a VI, 147 p. 1 illus. $b online resource.
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
347 $a text file $b PDF $2 rda
490 1 $a Surveys and Tutorials in the Applied Mathematical Sciences, $x 2199-4773 ; $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 2 4 $a Manifolds and Cell Complexes. $3 1366170
650 2 4 $a Symbolic and Algebraic Manipulation. $3 669944
650 2 4 $a Formal Languages and Automata Theory. $3 1365747
650 2 4 $a Algebraic Topology. $3 672209
650 1 4 $a Mathematical Logic and Foundations. $3 669393
650 0 $a Manifolds (Mathematics). $3 1051266
650 0 $a Computer science—Mathematics. $3 1253519
650 0 $a Machine theory. $3 527775
650 0 $a Algebraic topology. $3 678206
650 0 $a Mathematical logic. $2 bicssc $3 810627
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
776 0 8 $i Printed edition: $z 9783031146480
776 0 8 $i Printed edition: $z 9783031146503
830 0 $a Surveys and Tutorials in the Applied Mathematical Sciences, $x 2199-4765 ; $v 7 $3 1323024
856 4 0 $u https://doi.org/10.1007/978-3-031-14649-7
912 $a ZDB-2-SMA
912 $a ZDB-2-SXMS
950 $a Mathematics and Statistics (SpringerNature-11649)
950 $a Mathematics and Statistics (R0) (SpringerNature-43713)