東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Exploring formalisation = a primer i...

Loh, Clara.

Linked to FindBook

Google Book

Amazon

博客來

Exploring formalisation = a primer in human-readable mathematics in Lean 3 with examples from simplicial topology /

Record Type:	Electronic resources : Monograph/item
Title/Author:	Exploring formalisation/ by 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.
[NT 15003449]:	Introduction -- 1 The Lean Proof Assistant -- 2 Basic Examples -- 3 Design Choices -- 4 Abstraction and Prototyping.
Contained By:	Springer Nature eBook
Subject:	Automatic theorem proving - Computer programs. -
Online resource:	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 /
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. 11..

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:

3606370
Automatic theorem proving
--Computer programs.

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

Dewey Class. No.: 511.3

Exploring formalisation = a primer in human-readable mathematics in Lean 3 with examples from simplicial topology /
LDR:02307nmm a2200361 a 4500 001 2304274
003 DE-He213
005 20220924152834.0
006 m d
007 cr nn 008maaau
008 230409s2022 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 3270922
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 3606370
650 1 4 $a Mathematical Logic and Foundations. $3 892656
650 2 4 $a Algebraic Topology. $3 891269
650 2 4 $a Formal Languages and Automata Theory. $3 3592087
650 2 4 $a Symbolic and Algebraic Manipulation. $3 891222
650 2 4 $a Manifolds and Cell Complexes. $3 3538507
710 2 $a SpringerLink (Online service) $3 836513
773 0 $t Springer Nature eBook
830 0 $a Surveys and tutorials in the applied mathematical sciences ; $v v. 11. $3 3606369
856 4 0 $u https://doi.org/10.1007/978-3-031-14649-7
950 $a Mathematics and Statistics (SpringerNature-11649)