Formalising Mathematics In Simple Type Theory
Lawrence C. Paulson
TL;DR
This paper demonstrates that simple type theory is sufficient for formalising significant mathematical topics, comparing different proof assistants and formalisation techniques, and discusses the future adaptability of formal systems.
Contribution
It provides a comparative analysis of formalising mathematics in simple type theory using HOL Light and Isabelle/HOL, highlighting different approaches and future-proofing considerations.
Findings
Formal proofs of stereographic projections in HOL Light and Isabelle/HOL
Comparison of Harrison's Euclidean space formalisation with Isabelle/HOL's axiomatic type classes
Discussion on the evolution and future migration of formal systems
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsData Management and Algorithms · Computer Graphics and Visualization Techniques · Constraint Satisfaction and Optimization