001449921 000__ 02925cam\a2200481\i\4500
001449921 001__ 1449921
001449921 003__ OCoLC
001449921 005__ 20230310004425.0
001449921 006__ m\\\\\o\\d\\\\\\\\
001449921 007__ cr\cn\nnnunnun
001449921 008__ 220930s2022\\\\sz\a\\\\ob\\\\001\0\eng\d
001449921 020__ $$a9783031146497$$q(electronic bk.)
001449921 020__ $$a3031146492$$q(electronic bk.)
001449921 020__ $$z9783031146480
001449921 0247_ $$a10.1007/978-3-031-14649-7$$2doi
001449921 035__ $$aSP(OCoLC)1346304621
001449921 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dEBLCP$$dOCLCF$$dOCLCQ
001449921 049__ $$aISEA
001449921 050_4 $$aQA76.9.A96
001449921 08204 $$a511.3$$223/eng/20220930
001449921 1001_ $$aLöh, Clara,$$eauthor.
001449921 24510 $$aExploring formalisation :$$ba primer in human-readable mathematics in Lean 3 with examples from simplicial topology /$$cClara Löh.
001449921 264_1 $$aCham :$$bSpringer,$$c[2022]
001449921 264_4 $$c©2022
001449921 300__ $$a1 online resource (vi, 147 pages) :$$billustrations.
001449921 336__ $$atext$$btxt$$2rdacontent
001449921 337__ $$acomputer$$bc$$2rdamedia
001449921 338__ $$aonline resource$$bcr$$2rdacarrier
001449921 4901_ $$aSurveys and tutorials in the applied mathematical sciences,$$x2199-4773 ;$$vvolume 11
001449921 504__ $$aIncludes bibliographical references and index.
001449921 5050_ $$aIntroduction -- 1 The Lean Proof Assistant -- 2 Basic Examples -- 3 Design Choices -- 4 Abstraction and Prototyping.
001449921 506__ $$aAccess limited to authorized users.
001449921 520__ $$aThis 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.
001449921 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed September 30, 2022).
001449921 650_0 $$aAutomatic theorem proving$$xComputer programs.
001449921 655_0 $$aElectronic books.
001449921 830_0 $$aSurveys and tutorials in the applied mathematical sciences ;$$v11.$$x2199-4773
001449921 852__ $$bebk
001449921 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-031-14649-7$$zOnline Access$$91397441.1
001449921 909CO $$ooai:library.usi.edu:1449921$$pGLOBAL_SET
001449921 980__ $$aBIB
001449921 980__ $$aEBOOK
001449921 982__ $$aEbook
001449921 983__ $$aOnline
001449921 994__ $$a92$$bISE