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

28 Sep 2022 » Memories: Edinburgh LCF, Cambridge LCF, HOL88
Just over 40 years ago, 2 February 1982, I arrived at Heathrow to take up a postdoc under Mike Gordon and Robin Milner to work on Edinburgh LCF. Mike kindly met me at the airport and drove me to a room that he had organised himself (favours which I have sadly never offered to any of my visitors). This was the true start of my research career, leaving behind my offbeat PhD project and ultimately reconnecting with ideas I had picked up from NG de Bruijn: the formalisation of mathematics. Although I am best known for the development of Isabelle, most of my work in those early years went directly into the HOL system.
14 Sep 2022 » Porting Libraries of Mathematics Between Proof Assistants
In 2005, a student arrived who wanted to do a PhD involving formalised probability theory. I advised him to use HOL4, where theories of Lebesgue integration and probability theory had already been formalised; they were not available in Isabelle/HOL. Ironically, he eventually discovered that the HOL4 theories didn’t meet his requirements and he was forced to redo them. This episode explains why I have since devoted so much effort to porting libraries into Isabelle/HOL. But note: Isabelle/HOL already had, from 2004, a full copy of the HOL4 libraries, translated by importer tools. I never even thought of using these libraries, and they were quietly withdrawn in 2012. Why was that? And what is the right way to achieve interoperability between proof assistant libraries?
07 Sep 2022 » Ackermann's function is not primitive recursive, II
The previous post presented the first half of the proof that Ackermann’s function $A(i,j)$ is not primitive recursive: a series of inequalities describing how the function grows with various arguments. In this post, we’ll see how to define the primitive recursive functions inductively. Using the aforementioned inequalities, it will be straightforward to prove (by induction on the construction of some PR function f) that we can always find an argument to dominate f. This celebrated result has an easy proof, and it provides a distinctive example of an inductive definition.
31 Aug 2022 » Ackermann's function is not primitive recursive, I
A university-level course on computation theory will invariably cover recursive functions: the model of computation developed by Gödel and Kleene. Students learn about the primitive recursive (PR) functions, a fairly natural idea, but also learn that the PR functions are insufficient. True, these functions include all the familiar arithmetic operations, as well as all the obvious syntactic operations on expressions that have been “Gödel-numbered” (coded in terms of arithmetic formulas). Among the PR functions are many that cannot be regarded as feasibly computable because they grow at an utterly unimaginable rate. (Do not say “exponential”: in this context, exponential growth is negligible.) The PR functions are insufficient because, in three simple lines, we can define an obviously computable function that grows faster than any of them. It is, of course, Ackermann’s function.
17 Aug 2022 » BDDs in HOL: the coolest thing Mike Gordon ever did
On 22 August, it will be five years since the death of Mike Gordon, who • basically invented hardware verification • contributed to the first version of the ML programming language • made major contributions to proof assistant architecture, and • showed that higher-order logic was a powerful formalism for verification. My biography (also available here) describes his main achievements. But it is almost silent about the coolest thing he ever did: integrating binary decision diagrams (BDDs) with the HOL system.
10 Aug 2022 » The formalisation of nonstandard analysis
Calculus is concerned with change over infinitesimal intervals. Both Isaac Newton and Wilhelm Leibniz regarded infinitely small quantities as mathematically meaningful, and Leonhard Euler continued to work with infinitesimals and infinities even after Bishop Berkeley published his polemic against the practice in 1734. To be sure, Euler’s conception of infinitesimals seemed contradictory. His infinitesimal quantities were definitely and necessarily nonzero, but “vanishing” and therefore “really” equal to zero. Not until the 19th century were infinitesimals banished from mathematics by the $\epsilon$-$\delta$ arguments of Bolzano, Weierstraß and others. And then, in the 1960s, Abraham Robinson discovered a coherent and rigorous interpretation of infinitesimals. But is nonstandard analysis relevant to formalised mathematics?
03 Aug 2022 » A few small formalisation challenges
Novices getting to grips with interactive theorem proving need examples to formalise. When Russell O’Connor was getting to grips with Coq, he thought that a nice little exercise would be to formalise Gödel’s incompleteness theorem. I hope he will not be offended if I remark that that was a crazy idea, even though he was successful. Below, I list a few proofs that I would like to see formalised. I am not sure how easy they are, but all of them are easier than Gödel’s Theorem!
27 Jul 2022 » Mathematical truth, mathematical modelling and axioms
The recent COVID-19 pandemic has given us a striking demonstration of science in action. Over a period of two years, scientists around the world examined this unknown pathogen. They decoded its genome and developed vaccines and treatments. But some people were not impressed: since scientific advice could change from month to month, scientific truth was fallible. “Sceptics” preferred to rely on treatments advocated by quacks based on feeble evidence but promoted with absolute confidence. Some fell ill but continued to cling to quack advice and conspiracy theories until literally their dying breath. Scientific truth is regularly challenged by new observations. On the other hand, mathematical truth is infallible, right?
13 Jul 2022 » How Isabelle emerged from the trends of the 1980s
The fault lines of today’s proof assistant community are striking. In one corner are researchers into advanced constructive type theories. I get the impression (if Twitter is at all reliable) that they see their rivals as set theorists, though I’d be surprised if any set theorists were even aware of their work. Anyway, hardly anybody uses set theory in a proof assistant. Their true rivals with regard to interactive theorem proving are using classical simple type theory systems, such as Isabelle/HOL. But does anybody recognise the extent to which Isabelle has been influenced by type theories like AUTOMATH and Martin-Löf?
06 Jul 2022 » On Turing machines
Every now and then, somebody claims that Turing “invented the computer”, because he invented Turing machines. However, Turing machines are not designs of actual computing machines. They aren’t even abstract models of machines. It turns out (we have Turing’s own word for it), a TM is a model of a man writing on paper at a desk. So why did Turing invent TMs, and where did this lead?
22 Jun 2022 » What is the point of formalising mathematics?
Vladimir Voevodsky was a leading proponent of the formalisation of mathematics. Until his death in 2017, he lectured frequently on the risks of errors in complicated technical arguments and the necessity to start using computers to verify the work of mathematicians. The opinions of a Fields Medallist naturally carried weight. From the other side, the verification world, a major impetus for the formalisation of mathematics was the floating point division bug in the Pentium, back in 1994. (See my prior post on the ALEXANDRIA project.) However, Trybulec started his Mizar project in 1973, de Bruijn had created the first version of AUTOMATH by 1968, and Wang had built an automatic theorem prover already in 1958, in hope of eventually formalising mathematics. People have been dreaming about this for a long time. What is the point?
15 Jun 2022 » Formalising Ramsey theory, II
Unlike the natural sciences, which are confined to what actually exists in the universe, mathematics is limited only by our imagination. Some branches, such as number theory, attract much attention, while other topics languish in the fringes. One fringe topic is Ramsey theory, and if anybody has heard of it, it’s probably because it captured the attention of one of mathematics’ few celebrities: Paul Erdős. A previous post introduced Ramsey’s theorem itself. It’s reasonably well known and has significant applications. Things get more obscure when we move into the transfinite. In the sequel, you need to be familiar with ordinals, including ordinal arithmetic and order types.
08 Jun 2022 » Dealing with descriptions in Isabelle/HOL: least, greatest, whatever
A description is a term that designates “the least”, “the greatest” or simply “any” x such that Φ(x): it describes the desired value (or simply any suitable value) in the language of its properties. The built-in facts governing Min, Max, etc. are straightforward, but getting what you want from them is often frustrating. Let’s take a look at a few contrived, but (I hope) illustrative examples, leaving all the proofs to sledgehammer.
01 Jun 2022 » Formalising Gödel's incompleteness theorems, III: Coding and Bound Variables
Gödel’s proof uses arithmetic (or in our case, hereditarily finite sets) to encode logical syntax, rules of inference, and therefore theorems of the internal calculus. Analogous coding techniques are ubiquitous in computation theory, complexity theory and elsewhere in logic under the general heading of problem reduction: showing that something is impossible because it could otherwise be used to solve another problem already known to be impossible. A complication is that our calculus involves variable binding, with the attendant horrors of name clashes and renaming. As described in a previous post, the Isabelle/HOL formalisation of HF deals with variable binding through the nominal package, but when coding HF in itself we shall be forced to use a simpler technique, due to de Bruijn.
25 May 2022 » Formalising Gödel's incompleteness theorems, II: Σ-formulas
Gödel’s theorem, more than other deep results, is burdened with numerous tiresome definitions and lemmas. It’s necessary to codify in full the axioms and inference rules of HF, the internal logic, as well as a toolbox of derived syntactic primitives needed for expressing and proving HF statements. (It’s also necessary to prove that the primitives actually work, a particularly tiresome step that most authors omit.) Here, let’s look at something a bit more interesting: Świerczkowski’s Theorem 2.5, which states that every true Σ-sentence is a theorem. This turns out to be vital once we set up Gödel encodings of formulas and define a provability predicate, Pf. It will be possible to show that φ is a theorem if and only if Pf⌜φ⌝ is true, for any HF formula φ. The point is that all of these syntactic predicates can be defined as Σ-formulas. Therefore, if Pf⌜φ⌝ is true, we get—for free—that Pf⌜φ⌝ is formally provable. To get started, we first need to define Σ-formulas.
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.

Machine Logic

At the junction of computation, logic and mathematics

Archive

Posts