Formalising Mathematics Using Isabelle
Gödel’s Incompleteness Theorems
Gödel’s Incompleteness Theorems are among the most celebrated (and misunderstood) results in mathematics. The first incompleteness theorem states that every sufficiently strong formal theory has an undecidable sentence; the second incompleteness theorem states that no such formal system can prove a theorem that is logically equivalent to its own consistency. While the first theorem has been mechanised using a number of proof assistants as early as 1986, the second incompleteness theorem has never been mechanised until now. The two papers below describe the work (1) for logicians and (2) for researchers in automated reasoning. The proof scripts and slides are also available.
- L. C. Paulson.
A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets.
Review of Symbolic Logic 7 3 (2014), 484–498. Publisher's version at journals.cambridge.org
© Association for Symbolic Logic, 2014 - L. C. Paulson.
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle.
J. Automated Reasoning 55 1 (2015), 1–37. Publisher's version at www.springerlink.com
Finite Automata and Regular Languages
This paper describes a small development that demonstrates the utility of hereditarily finite set theory in formalising mathematics.
- L. C. Paulson. A formalisation of finite automata using hereditarily finite sets.
In: Amy P. Felty and Aart Middeldorp (editors), 25th International Conf. on Automated Deduction: CADE-25 (Springer LNAI 9195, 2015), 231–245. Publisher's version at www.springerlink.com
Formalising Set Theory
Axiomatic set theory is the foundation of mathematics, but for most people it is obscure and incomprehensible. The papers described below concern Isabelle/ZF, which provides an interactive environment for undertaking set theory proofs. Isabelle's architecture, based on a logical framework, allows it to support ZF set theory within the context of first-order logic. The highlight of this work is the formalisation of Gödel's constructible universe, a feat that cannot even be attempted using most verification tools.
- L. C. Paulson.
Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389. Publisher's version at www.springerlink.com - L. C. Paulson.
A fixedpoint approach to implementing (co)inductive definitions (revised version). In: A. Bundy (editor), 12th International Conf. on Automated Deduction (Springer LNAI 814, 1994), 148–161.
Slides available • Publisher's version at www.springerlink.com - L. C. Paulson.
Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215. Publisher's version at www.springerlink.com - L. C. Paulson and Krzysztof Grabczewski.
Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. Slides available • Publisher's version at www.springerlink.com - L. C. Paulson.
Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567. - L. C. Paulson.
The reflection theorem: a study in meta-theoretic reasoning.
In: A. Voronkov (editor), 18th International Conf. on Automated Deduction: CADE-18 (Springer LNAI 2392, 2002), 377–391. Publisher's version • Slides available - L. C. Paulson.
The relative consistency of the axiom of choice — mechanized using Isabelle/ZF.
LMS J. Computation and Mathematics 6 (2003), 198–248. Slides and theory document available
General Mathematics
- J. Fleuriot and L. C. Paulson.
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. In: Xiao-Shan Gao, Dongming Wang and Lu Yang (editors), Automated Deduction in Geometry, Second International Workshop, ADG '98 (Springer LNCS 1669, published 1999), 47–66. - F. Kammüller and L. C. Paulson.
A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle HOL. J. Automated Reasoning 23 (1999), 235–264. - L. C. Paulson.
Defining Functions on Equivalence Classes. ACM Trans. on Computational Logic 7 4 (2006), 658–675. Slides available - Wenda Li and L. C. Paulson. A formal proof of Cauchy's residue theorem. In: Jasmin C. Blanchette and Stephan Merz (editors), ITP 2016: Seventh International Conference on Interactive Theorem Proving (Springer LNCS 9807), 235–251. Publisher's version at www.springerlink.com
Supported by the ERC Advanced Grant ALEXANDRIA
- Mohammad Abdulaziz and L. C. Paulson.
An Isabelle/HOL formalisation of Green’s theorem.
J. Automated Reasoning 63:3 (2019), 763–786. Publisher's version - L. C. Paulson.
Formalising mathematics in simple type theory.
In: Stefania Centrone, Deborah Kant and Deniz Sarikaya (editors), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts (Springer, 2019), 437–453. Publisher's version - Wenda Li and L. C. Paulson.
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL.
J. Automated Reasoning 64:2 (2020), 331–360. - Paulo Emílio de Vilhena and L. C. Paulson.
Algebraically closed fields in Isabelle/HOL.
In: Nicolas Peltier and Viorica Sofronie-Stokkermans (editors), IJCAR 2020 — Automated Reasoning, 10th International Joint Conference, Part II (Springer LNCS 12167, 2020), 204–220. Publisher's version - Chelsea Edmonds and L. C. Paulson.
A modular first formalisation of combinatorial design theory.
In: Fairouz Kamareddine and Claudio Sacerdoti Coen (editors), Intelligent Computer Mathematics (Springer LNCS 12833, 2021), 3–18. Publisher's version - Angeliki Koutsoukou-Argyraki, Wenda Li and L. C. Paulson.
Irrationality and transcendence criteria for infinite series in Isabelle/HOL.
Experimental Mathematics 31:2 (2022), 401–412. - Mirna Džamonja, Angeliki Koutsoukou-Argyraki and L. C. Paulson.
Formalising ordinal partition relations using Isabelle/HOL.
Experimental Mathematics 31:2 (2022), 383–400. - Anthony Bordg, L. C. Paulson and Wenda Li.
Simple type theory is not too simple: Grothendieck's schemes without dependent types.
Experimental Mathematics 31:2 (2022), 364–382. - Chelsea Edmonds and L. C. Paulson.
Formalising Fisher’s inequality: formal linear algebraic proof techniques in combinatorics.
In: June Andronick and Leonardo de Moura (editors), 13th International Conference on Interactive Theorem Proving (2022), 11:1–19. Slides available - L. C. Paulson.
Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis.
In: Kevin Buzzard and Temur Kutsia (editors), Intelligent Computer Mathematics. (Springer LNAI 13467, 2022), 92–106. Slides available - Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and L. C. Paulson.
Formalising Szemerédi's regularity lemma and Roth's theorem on arithmetic progressions in Isabelle/HOL. Journal of Automated Reasoning 67:1 (2023). - L. C. Paulson.
A formalised theorem in the partition calculus.
Annals of Pure and Applied Logic 175 (2024). Publisher's version - Chelsea Edmonds and L. C. Paulson.
Formal probabilistic methods for combinatorial structures using the Lovász local lemma.
In: Brigitte Pientka and Sandrine Blazy (editors), CPP 2024: ACM SIGPLAN International Conference on Certified Programs and Proofs (2024), 132–146. Publisher's version • Slides available - Manuel Eberl, Anthony Bordg, L. C. Paulson and Wenda Li.
Formalising half of a graduate textbook on number theory.
In: Yves Bertot, Temur Kutsia and Michael Norrish (editors), 15th International Conference on Interactive Theorem Proving (2024), 40:1–7.