# 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*.*Xiao-Shan Gao, Dongming Wang and Lu Yang (editors),*In*:*Automated Deduction in Geometry, Second International Workshop, ADG '98* - 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 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