Language:
English
繁體中文
Help
Login
Back
Switch To:
Labeled
|
MARC Mode
|
ISBD
Exploring Formalisation = A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /
Record Type:
Language materials, printed : Monograph/item
Title/Author:
Exploring Formalisation/ by Clara Löh.
Reminder of title:
A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology /
Author:
Löh, Clara.
Description:
VI, 147 p. 1 illus.online resource. :
Contained By:
Springer Nature eBook
Subject:
Mathematical logic. -
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 /
Löh, Clara.
Exploring Formalisation
A 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:
810627
Mathematical logic.
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
0
$a
Mathematical logic.
$2
bicssc
$3
810627
650
0
$a
Algebraic topology.
$3
678206
650
0
$a
Machine theory.
$3
527775
650
0
$a
Computer science—Mathematics.
$3
1253519
650
0
$a
Manifolds (Mathematics).
$3
1051266
650
1 4
$a
Mathematical Logic and Foundations.
$3
669393
650
2 4
$a
Algebraic Topology.
$3
672209
650
2 4
$a
Formal Languages and Automata Theory.
$3
1365747
650
2 4
$a
Symbolic and Algebraic Manipulation.
$3
669944
650
2 4
$a
Manifolds and Cell Complexes.
$3
1366170
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)
based on 0 review(s)
Multimedia
Reviews
Add a review
and share your thoughts with other readers
Export
pickup library
Processing
...
Change password
Login