The formal verification of computer systems has become practical. It has an essential role in tech firms such as Amazon, AMD, Intel, Microsoft and Nvidia. In recent years, researchers have started asking whether verification technology could also benefit research mathematicians. Here, we explore every aspect of doing logic on the computer: its foundations, its applications and the issues involved with formalising mathematics.

Posts

• 18 May 2022 » Formalising Gödel's incompleteness theorems, I

  Gödel’s incompleteness theorems state limits on formal systems. (1) A consistent system strong enough to express the basic properties of integer addition and multiplication must be incomplete: there exists a formula that is neither provable nor refutable within the system, and (2) no such formal system can prove its own consistency. The first theorem is proved by using integer arithmetic to encode logical formulas, operations on them such as substitution, and inference according to the rules of the formal system. A fixedpoint construction yields an explicit formula expressing its own unprovability. The technical complications of the first theorem are formidable but were overcome already by Shankar in the 1980s and again by John Harrison and Russell O’Connor. This post introduces my own formalisation, using Isabelle/HOL. It also demonstrates formalising syntax involving variable binding using the nominal package of Christian Urban and Stefan Berghofer. More generally, it illustrates how to specify the syntax, semantics and proof theory of a formal system.

• 11 May 2022 » Getting started: basic Isabelle/jEdit tricks

  As mentioned last time, proof assistants can be daunting, and it’s not just about how to prove theorems. It’s about being aware of all the bells and whistles provided to help you prove theorems. The first modern proof assistant, Edinburgh LCF, provided nothing but a top-level to the ML programming language, designed specifically to the Meta Language for proving theorems. It was a bare-bones environment, but at least it was Turing complete! Nowadays, things work differently. This post is mainly for beginners, but experienced users might learn something too.

• 04 May 2022 » Getting started with Isabelle: baby examples, cool proof methods

  For absolute beginners, proof assistants are daunting. Everything you do seems to go wrong. So let’s have some super simple examples that show how to get started while highlighting some pitfalls.

• 27 Apr 2022 » Wetzel's problem and the continuum hypothesis

  The continuum hypothesis (CH) dates from the 19th century and became the first of David Hilbert’s famous unsolved problems. Gödel proved it to be consistent with the axioms of set theory (ZFC), while Cohen exhibited models of ZFC in which CH failed. New axioms would be needed to settle the question. Despite decades of intensive research, the status of CH remains open. However recondite it may be, CH cannot be ignored: ordinary-looking mathematical questions occasionally bump into it.

• 20 Apr 2022 » Why are you being constructive?

  Four decades ago, I was in a hi-fi shop looking at portable cassette players. Metal tapes had just come out, and metal-compatible cassette players were marketed with METAL emblazoned on the packaging. Three boys aged about 12 rushed into the shop. “That one’s got metal!”, shouted one. “This one’s got metal too!” shouted another. The third boy kept asking, “But does that make it sound better?” They ignored him.

• 13 Apr 2022 » Sledgehammer: some history, some tips

  Sledgehammer is the subsystem that links Isabelle/HOL to automatic theorem provers like Vampire and Z3. It is so much part of the Isabelle user’s everyday experience that it can be hard to remember a time before it was there. Let’s see if I can dig up some memories, and also come up with some usage tips relevant today.

• 06 Apr 2022 » Integrating Zermelo-Fraenkel set theory with higher-order logic

  Many researchers, frustrated with the limited expressiveness of higher-order logic vis-à-vis Zermelo Frankel set theory, have sought somehow to combine the two. The difficulty is to make the combination seamless, yielding a unified formal theory rather than two theories bolted together. We don’t want to keep transferring facts, constructions and proofs from one theory to the other.

• 30 Mar 2022 » Equivalence classes and quotienting

  A quotient construction partitions a set according to ∼, some equivalence relation. The equivalence classes — members of the partition — are maximal sets of ∼-equivalent elements. To use computer science jargon, the construction yields an abstract type (the equivalence classes) and the elements of those classes belong to an underlying concrete type. For example, pairs of natural numbers can represent integers or nonnegative rationals, depending on the equivalence relation chosen. However, quotienting has nothing to do with types.

• 23 Mar 2022 » Type classes versus locales

  As we’ve seen in an earlier post, type classes are a convenient mechanism for managing the overloading of syntax in a principled manner: types share syntax and related properties. For example, the familiar arithmetic operators share commutative, distributive and associative laws on numeric types as different as the integers and the complex numbers. We also saw how to introduce a new type (of quaternions) and quickly bring it “into the fold” of arithmetic types through a few instance declarations. The main limitation of type classes is that the syntax and properties are associated with a type, exactly one type, and in only one way. Locales manage syntax and axioms in a more general way, e.g. to deal with abstract algebra.

• 16 Mar 2022 » Types versus sets (and what about categories?)

  A recent Twitter thread brought home to me that there is widespread confusion about what types actually are, even among the most prominent researchers. In particular: are types the same thing as sets? At the risk of repeating some of my prior posts, perhaps it’s time for a little history about type theory, set theory and their respective roles as foundations of mathematics.

• 09 Mar 2022 » The quaternions—and type classes

  The quaternion number system is an extension of the complex numbers to 4 dimensions, introduced by Hamilton in 1843. I translated the HOL Light formalisation of quaternions into Isabelle/HOL some time ago. One notable feature of the formalisation (taken from the Isabelle/HOL formalisation of the complex numbers) is that its definition can be regarded as coinductive. Moreover, continuing the previous post about axiomatic type classes, we have a dramatic demonstration of how quickly a new class of numbers can be made native (so to speak).

• 02 Mar 2022 » Axiomatic type classes: some history, some examples

  Type classes now play a major role in all the leading proof assistants: Coq, Lean and of course Isabelle/HOL. They have come a long way from their origins in the world of functional programming languages. They were mentioned in the previous post, so let’s take a closer look.

• 23 Feb 2022 » The hereditarily finite sets

  A set is hereditarily finite if it is finite and all of its elements are hereditarily finite. They satisfy the axioms of set theory with the negation of the axiom of infinity. There are countably many HF sets, and they are a natural domain for formalising computation. They also allow a straightforward treatment of Gödel’s incompleteness theorems.

• 16 Feb 2022 » A classical proof: exponentials are irrational

  In Proofs from THE BOOK, Aigner and Ziegler present hundreds of classic proofs from what we might call the mathematical canon, based in large part on suggestions by Paul Erdős. The authors confine themselves to proofs requiring “only a modest amount of technique from undergraduate mathematics”. Nothing too advanced or specialised, but nevertheless, a selection of insightful techniques across the mathematical landscape. Here we look at an Isabelle/HOL proof that the exponential function yields irrational numbers.

• 09 Feb 2022 » Fun with Ackermann's function

  An undergraduate course on recursion theory typically introduces Turing machines, register machines, general recursive functions and possibly the λ-calculus. They learn about the principle of primitive recursion, which is easy to grasp, and the minimisation operator, which is less so. Ackermann’s function is invariably mentioned as an example of a function that is obviously computable but not computable by primitive recursion alone. Unfortunately, it is not easily expressible in the familiar models of computation, although its definition is simplicity itself.

• 02 Feb 2022 » Formalising mathematics in set theory

  Last week’s post mentioned the mechanisation of some major results of ZF set theory in proof assistants. In fact, the use of automated theorem provers with various forms of set theory goes back a long way. Two stronger set theories have attracted interest: von Neumann–Bernays–Gödel (NBG) and Tarski–Grothendieck (TG). All of this work was motivated by the goal of mechanising mathematics.

• 26 Jan 2022 » Is Zermelo-Fraenkel set theory the foundation of mathematics?

  Set theory (specifically, ZFC) is said to be the foundation of mathematics. Who says so, and are they right? How do our various typed formalisms compare to set theory? What about set theory as a branch of mathematics to be mechanised?

• 19 Jan 2022 » Formalising extremal graph theory, I

  Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and I recently formalised Roth’s theorem on arithmetic progressions. The project required first formalising Szemerédi’s regularity lemma, which “states that the vertices of every large enough graph can be partitioned into a bounded number of parts so that the edges between different parts behave almost randomly” (Wikipedia). The mathematics is elementary enough. Our main difficulties were caused by ambiguities, not merely in the proofs but in the statements of the theorems and even the definitions.

• 12 Jan 2022 » Proving the obvious

  It is commonly opined that proof assistants are useless for mathematics because they are too difficult to learn and use. This opinion is incorrect: I am as skilled as anyone on the planet at using Isabelle/HOL, but no amount of skill can compensate for the limitations of today’s tools. They are simply too stupid to prove obvious things.

• 05 Jan 2022 » The de Bruijn criterion vs the LCF architecture

  A key objective of formalising mathematics is to ensure its correctness. We have previously considered how we can know whether a given logical formalism is faithful to mathematical reasoning. That raises another question: given the prevalence of errors in computer programs, how can we guarantee that our proof assistants are correct? Two separate approaches are the de Bruijn criterion and the LCF architecture, and I’d like to advocate a third.

• 29 Dec 2021 » Formalising Ramsey theory, I

  To quote Herbert Ryser, Ramsey’s theorem is “a profound generalisation” of the pigeon-hole principle, which “asserts that if a set of sufficiently many elements is partitioned into not too many subsets, then at least one of the subsets must contain many of the elements”. Ramsey’s theorem initiated a new branch of infinitary combinatorics and is also the key to today’s software termination checkers.

• 22 Dec 2021 » Readability in proofs: the mean value theorem

  Doing mathematics requires a combination of intuition and rigour. Intuition is the source of ideas and conjectures. Proofs need to be rigorous, while at the same time avoiding excessive detail, which would destroy readability. That is why we need intuition even to read a proof, let alone to conceive the theorem in the first place. How can we capture intuition in a formal proof?

• 15 Dec 2021 » Do Gödel's incompleteness theorems matter?

  Gödel’s incompleteness theorems are often regarded as placing strict limits on the power of logic. Don’t they immediately imply that any project to formalise mathematics is doomed to fail?

• 08 Dec 2021 » ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician

  ALEXANDRIA is an ERC Advanced Grant with the aim of making verification technology — originally designed to verify computer systems — useful in the practice of professional mathematics. Another project with similar aims has developed around Lean, a proof assistant based on essentially the same type theory as Coq. Without doubt the idea of doing mathematics by machine is in the air. But why?

• 01 Dec 2021 » Undefined values, or what do we get when we divide by zero?

  One perplexing issue, especially for newcomers to machine proof, is the question of undefined values: whether from division by zero or from a non-existent limit, integral or other sophisticated concept. This issue produces strong opinions and some proposed solutions are radical. But for many proof assistants the solution is basically “don’t worry about it”.

• 24 Nov 2021 » Intuitionism and constructive logic

  Intuitionism was for most of the 20th century a recondite topic in the foundations of mathematics. But in the 1970s, the emergence of constructive type theories, and simultaneously, functional programming languages, brought these topics to the forefront of theoretical computer science. Many practitioners of machine logic (particularly those using Coq) strive to create constructive (as opposed to classical) proofs.

• 17 Nov 2021 » An Experiment: The Cauchy–Schwarz inequality

  The Cauchy–Schwarz inequality is a well-known fact about vector inner products. It comes in various forms that any mathematician is expected to recognise.

• 10 Nov 2021 » The axiom of choice and descriptions

  Few topics in mathematics are more contentious––or misunderstood––than the axiom of choice. We adopt it in the form of Hilbert’s ε-operator.

• 03 Nov 2021 » NG de Bruijn and AUTOMATH

  NG de Bruijn visited Caltech in the spring of 1977 to deliver a course on his AUTOMATH mathematical language. I was lucky enough to attend and to have private discussions with him.

• 27 Oct 2021 » On logical formalisms

  Looking at the previous example, on Fibonacci numbers, you may be wondering, how we can be sure that a machine proof corresponds to actual mathematics? This question raises complex issues in the foundations of mathematics and logic.

• 20 Oct 2021 » More on Fibonacci numbers, with equational reasoning

  The previous post introduced a definition of the Fibonacci function along with some simple proofs by induction. We continue our tour with examples of equational reasoning. Chains of equalities and inequalities are common in proofs and a proof assistant should allow them to be written.

• 13 Oct 2021 » Introductory example: Fibonacci numbers

  Let’s see what mathematics looks like in Isabelle/HOL. This post is not a self-contained tutorial; it simply aims to show a simple recursive definition and a couple of proofs by induction. Some good (and bad) points about machine proof should become obvious. There are links to further reading at the end.

• 09 Aug 2021 » Welcome to Machine Logic!

  This blog will cover a variety of topics connected with automated theorem proving and its applications, such as computer system verification and formalised mathematics. It’s aimed at readers who have some grasp of formal proofs already, perhaps from an undergraduate course on discrete mathematics or symbolic logic. There will be tutorial posts on such mysteries as LCF, intuitionism and inductive reasoning. Many posts will be overviews of work published elsewhere, so this blog will also function as a shop window into the vast literature on computational logic.