Formalising Mathematics in Simple Type Theory
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Paulson, LC
Abstract
Despite the considerable interest in new dependent type theories, simple type theory (which dates from 1940) is sufficient to formalise serious topics in mathematics. This point is seen by examining formal proofs of a theorem about stereographic projections. A formalisation using the HOL Light proof assistant is contrasted with one using Isabelle/HOL. Harrison's technique for formalising Euclidean spaces is contrasted with an approach using Isabelle/HOL's axiomatic type classes. However, every formal system can be outgrown, and mathematics should be formalised with a view that it will eventually migrate to a new formalism.
Description
Keywords
cs.LO, cs.LO, 03A05
Journal Title
CoRR
Conference Name
Journal ISSN
0166-6991
2542-8292
2542-8292
Volume Title
407
Publisher
Springer International Publishing
Publisher DOI
Rights
All rights reserved
Sponsorship
European Research Council (742178)