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

14 Oct 2024 » The λ-calculus, 2: the Church-Rosser theorem
A well-known technique to speed up computer code is to re-order some steps, for example to lift a costly operation out of a loop. In logic, when we can choose what inference to do next, making the right choices yields an exponentially shorter proof. Also in the λ-calculus we sometimes have a choice of reduction steps: the possible outcomes include, at one extreme, terminating exponentially faster or at the opposite extreme, not terminating at all. But it would certainly be vexing if two terminating computations could return different final values. Church and Rosser proved that couldn’t happen, implying the consistency of the λ-calculus and giving us some of the tools needed to study this question in other situations.
30 Sep 2024 » Introduction to the λ-calculus
The λ-calculus has had a pervasive impact on computer science – and not just in functional programming languages, most of which can be viewed as extended λ-calculi, but even in modern systems programming languages such as Rust. Polymorphic type checking emerged in the context of the typed λ-calculus and now exists (to some extent) in many modern languages. Turning to theory, denotational semantics is normally expressed within a form of λ-calculus. Both higher-order logic and dependent type theories are extensions of the λ-calculus. But it is a mysterious beast: let’s take a look.
21 Aug 2024 » Probabilistic reasoning and formal proof
Many are the pitfalls awaiting anybody trying to formalise a proof, but the worst are appeals to intuition. These are typically a sign that the author can’t be bothered to outline a calculation or argument. Perhaps the claim is obvious (to them, not to you). Probabilistic claims, say about drawing coloured balls from a sack, may look particularly dubious. But as Paul Erdős has shown, such arguments can yield short, intuitive proofs that are absolutely rigorous. To formalise them simply requires a bit of measure theory boilerplate.
08 Aug 2024 » A tricky lower bound proof
The previous post concerned exact numerical calculations, culminating in an example of establishing – automatically – a numerical lower bound for a simple mathematical formula. Although automation is the key to the success of formal verification, a numerical approach is not always good enough. In that example, we could get three significant digits quickly, four significant digits slowly and the exact lower bound never. As every calculus student knows, to locate a minimum or maximum you take the derivative and solve for the point at which it vanishes. The desired property can then be shown using the main value theorem. Let’s do it!
25 Jul 2024 » The mysteries and frustrations of numerical proofs
Sometimes the smallest details are the worst. What do we mean by 2+2=4? There are many different kinds of numbers: integers, rationals, reals, etc. It should not affect the answer, and mathematical writing takes advantage of that fact, but formalised mathematics has to be unambiguous. A further complication is that the various kinds of numbers are used in distinctive ways, e.g. recursion is only for the natural numbers. How do we reconcile the zero-versus-successor conception of the naturals with the need to work with decimal constants or large integers? Let’s see how it’s done in Isabelle/HOL.
28 Feb 2024 » Two small examples by Fields medallists
A couple of weeks ago, Tim Gowers posted on Twitter an unusual characterisation of bijective functions: that they preserve set complements. Alex Kontorovich re-tweeted that post accompanied by a Lean proof detailing Gowers’ argument. I took a look, and lo and behold! Isabelle can prove it with a single sledgehammer call. (That one line proof isn’t necessarily the best proof, however. Remember, we want proofs that are easy to read and maintain.) And Terrence Tao published a small example on Mastodon; let’s look at that one too.
14 Feb 2024 » Contradictions and the Principle of Explosion
That logic should be free from contradiction is probably its most fundamental principle, dating back to Aristotle. As described last time, the emergence of a contradiction in set theory – in the form of Russell’s paradox – was catastrophic. Few question the claim that no statement can be both true and false at the same time. But the law of contradiction is widely associated with something else, the principle of explosion: ex contradictione quodlibet, a contradiction implies everything. This principle has been disputed. One can formulate predicate logic without it: minimal logic.
And allegedly a student challenged Bertrand Russell by saying “suppose 1=0; prove that you are the Pope”. Russell is said to have replied that if 1=0 then 2=1 and therefore the 2-element set consisting of himself and the Pope actually contains only one element. It’s an amusing tale, but is the argument rigorous?
31 Jan 2024 » Russell's Paradox: myth and fact
The story of Russell’s paradox is well known. Gottlob Frege had written a treatise on the foundations of arithmetic, presenting a formal logic and a development of elementary mathematics from first principles. Bertrand Russell, upon reading it, wrote to Frege mostly to praise the work, but asking a critical question. Frege replied to express his devastation at seeing his life’s work ruined. Some later commentators went further, saying that Russell’s paradox refuted the entire logicist approach to the foundations of mathematics (the idea that mathematics can be reduced to logic). Much is wrong with this story. The impact of Russell’s paradox is less than many believe, and greater.
08 Nov 2023 » Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel
Coinduction has a reputation for being esoteric, but there are some situations where it is close to indispensable. One such scenario arose during an Isabelle refinement proof for a verified automatic theorem prover for first-order logic, a proof that also involved Anders Schlichtkrull. In that prover, execution traces can be finite or infinite, reflecting the undecidability of first-order logic. The refinement proof involves a simulation argument between two layers: an abstract specification and a concrete theorem prover, both given as transition systems (i.e., binary relations over states). A single “big” step of the concrete prover represents an entire iteration of the prover’s main loop and may therefore correspond to multiple “small” steps of the abstract prover.
01 Nov 2023 » What do we mean by "the foundations of mathematics"?
The phrase “foundations of mathematics” is bandied about frequently these days, but it’s clear that there is widespread confusion about what it means. Some say that a proof assistant must be based on a foundation of mathematics, and therefore that the foundations of mathematics refers to some sort of formal system. And yet, while set theory is frequently regarded as the foundation of mathematics, none of the mainstream proof assistants are based on set theory. These days we see everything from category theory to homotopy type theory described as a possible foundation of mathematics. There is a lot of wrongness here.
04 Oct 2023 » The concept of proof within the context of machine mathematics
This post is prompted by a preprint, Automated Mathematics and the Reconfiguration of Proof and Labor, recently uploaded by Rodrigo Ochigame. It begins by contrasting two opposing ideals of proof — what any computer scientist would call top-down versus bottom-up – and then asks how they might have to be modified in a possible future in which mathematics is automated. To my way of thinking, his outlook is too negative.
31 Aug 2023 » The End (?) of the ALEXANDRIA project
Today marks the final day of the ALEXANDRIA project. I outlined a brief history of the project not long ago. It is nevertheless right to take a moment to thank the European Research Council for funding it and to state, yet again, what the outcomes were. Six years on, what have we learned?
23 Aug 2023 » Propositions as types: explained (and debunked)
The principle of propositions as types (a.k.a. Curry-Howard isomorphism), is much discussed, but there’s a lot of confusion and misinformation. For example, it is widely believed that propositions as types is the basis of most modern proof assistants; even, that it is necessary for any computer implementation of logic. In fact, propositions as types was found to be unworkable as the basis for conducting actual proofs the first time it was tried, in the earliest days of the AUTOMATH system. All of the main proof assistants in use today maintain a clear distinction between propositions and types. The principle is nevertheless elegant, beautiful and theoretically fruitful.
09 Aug 2023 » When is a computer proof a proof?
In 1976, Appel and Haken caused delight mixed with consternation by proving the celebrated four colour theorem, but with heavy reliance on a computer calculation. An assembly language program was used to check 1936 “reducible configurations”; people were rightly concerned about errors in the code. However, the Appel–Haken proof also required “the investigation by hand about ten thousand neighbourhoods of countries with positive charge”,¹ much of which was done by Appel’s 13-year-old daughter, and nobody seemed bothered about the possibility of errors there. Computer algebra systems were emerging around that time and would eventually become widely used in many branches of science and engineering, although I can’t imagine a computer algebra calculation being uncritically accepted by any mathematics journal. Today, I and others hope to see mathematicians using proof assistants in their work. Whether machine proofs will be accepted as valid requires serious thought about the nature of mathematical proof. We have come a long way since 1976, but many mathematicians still distrust computers, and many struggle to agree on the computer’s precise role.
1. Robin Wilson, Four Colours Suffice: How the Problem Was Solved (Princeton, 2002) ↩
26 Jul 2023 » Hao Wang on the formalisation of mathematics
Since I have already devoted a blog post to a wildly overrated philosopher who barely understood logic, it’s time to pay tribute to an underrated philosopher who wrote thoughtfully and presciently on the formalisation of mathematics: Hao Wang. Wang must be seen primarily as a philosopher in the traditional sense, who wrote essays and books, but he also wrote code. He is the creator of the first truly powerful automatic theorem prover, using what we now know as a tableau method. Indeed, most of today’s technology for automated deduction has its origins in the work of philosophers — we can add Hilary Putnam and J Alan Robinson – who decided to write more than just words.
12 Jul 2023 » Porting the HOL Light metric space library
I’m sorry that there have been no posts since April. I’ve been busy with a side project: porting the HOL Light metric space library to Isabelle in time for the upcoming release. It was a big job: the chunk I grabbed initially comprised some 1335 lemmas, over 24K lines and nearly 1.2M bytes. Some of the lemmas turned out to have been ported previously, or otherwise turned out to be unnecessary; on the other hand, quite a few additional lemmas were needed. The material included metric spaces and many associated concepts, advanced material about toplogical spaces, the relationships among different kinds of spaces, and finally closure properties, especially under general products. Major contributions include Urysohn’s lemma and the Tietze extension theorem, the Baire Category Theorem and the Banach Fixed-Point Theorem.
27 Apr 2023 » The ALEXANDRIA Project: what has been accomplished?
One of the my first posts described ALEXANDRIA, my ERC Advanced Grant aiming to bring verification technology to professional mathematicians. This project ends on 31 August 2023 (extended by a year on account of the pandemic), so it’s surely time to update the community on what has been accomplished. As outlined in the earlier post, our starting point was a growing acceptance of the prevalence of errors in mathematics, along with a small body of formal mathematical developments that had been undertaken in a variety of proof assistants. We would mainly be using Isabelle/HOL, which had been designed to be agnostic as to applications but strongly influenced by the verification needs of computer scientists, not mathematicians. There was a detailed research proposal, as is always required, but our real strategy was simply to push things as hard as we could to see what obstacles we would bump into.
12 Apr 2023 » Wittgenstein on natural science, mathematics and logic
In a blog devoted to mathematics and logic, it’s hard to avoid Wittgenstein. Wittgenstein saw his main contributions being to the philosophy of mathematics and logic. I’m not sure that he understood either of them. But let’s begin with natural science, since it touches on topics relevant to this blog, such as the relationship between models and the real world. Natural science is another field where Wittgenstein indulged in his habit of obscurantism. Since I don’t know much about philosophy, perhaps I have no business criticising a famous philosopher. But I have the right to judge whether he is basing his reasoning on premises that are, if not correct, at least plausible.
22 Mar 2023 » Small examples involving binomial coefficients
The binomial coefficients, which appear in the binomial theorem, have numerous applications in combinatorics and the analysis of algorithms. Donald E Knuth wrote extensively about them in the book Concrete Mathematics. They are the elements of Pascal’s triangle and satisfy a great many mathematical identities. Let’s prove some of them using Isabelle/HOL. These and many more are available built-in.
08 Mar 2023 » The semantics of a simple functional language
The simplest way to precisely specify the meanings of programming language expressions is through an operational semantics. Such a definition consists of a set of what look like the inference rules of a logic, stating the conditions under which a given expression can be reduced to a value, or at least evaluated one step more. Formally, this sort of specification is an inductive definition, equipped with an induction principle for proving that a property holds for all executions. Such proofs are conceptually trivial—they involve checking that the property holds initially and that it is preserved by each execution step—but are extremely tedious to write out by hand. Fortunately, they are often trivial with the help of a little automation. Let’s prove a Church–Rosser property: that expression evaluation always leads to a unique final result.
22 Feb 2023 » Verifying the binary algorithm for greatest common divisors
The Euclidean algorithm for the GCD is generally regarded as one of the first algorithms worthy of the name –– its main competitor perhaps the sieve of Eratosthenes, for generating prime numbers. Euclid’s algorithm requires repeated calculations of integer remainders, which was a heavy operation on early computers. (Some provided no hardware to perform multiplication and division.) One can replace the remainder operation by subtraction. That algorithm is far too slow, especially if one of the arguments is much smaller than the other, but it can be refined to achieve high performance by noting that any binary computer can efficiently divide by two. Let’s verify this algorithm, and along the way see how inductive definitions are done in Isabelle/HOL.
08 Feb 2023 » An irrationality proof involving cube roots
According to myth, the discovery that √2 was irrational so horrified the students of Pythagoras that it was kept secret upon pain of death. Its irrationality was thought to be paradoxical because √2 could be constructed as the hypotenuse of a right triangle, and therefore definitely “existed”, while all numbers were assumed to be rational. A while back, I formalised a new proof of the irrationality of √2. Just recently, I stumbled upon an exam question: to prove the irrationality of ∛2+∛3. Its proof uses different techniques, but it’s not at all hard. Why not pause for a moment to prove it for yourself before looking at the formal treatment below?
01 Feb 2023 » On the infinite
One can’t do mathematics without thinking about infinity. And yet infinity seems to lead to every sort of paradox. One of these is Thomson’s Lamp , which is alternately switched on and off at geometrically decreasing intervals, so that within two minutes it has been switched on and off infinitely many times: after which, will it be on or off? Ninety-nine years ago, David Hilbert delivered a lecture entitled “On the Infinite”, which comes down to us as an essay. The famous Hilbert Hotel, with its infinitely many rooms, which even when full can make space for infinitely many additional guests, was apparently described in this lecture, although Hilbert left it out of his essay. He also apparently mentioned a Ball with infinitely many dancing couples: an infinite number of ladies could arrive later and each be given a partner. I hope that the music was audible. How can we make sense of all this?
18 Jan 2023 » Formalising a new proof that the square root of two is irrational
Recently, somebody shared on Twitter a new proof of the irrationality of √2. Its claimed advantage is that “it requires no knowledge of mathematics above the definition of what it means for a number to be irrational, and can be written almost in one line.” These claims are dubious: the usual proof, which I’ve formalised in a previous post, requires only the natural numbers and the notion of divisibility. The “beautiful” proof involves real numbers, potentially infinite sets and the nontrivial claim that the square root of two actually exists. Nevertheless, formalising it in Isabelle/HOL is an interesting exercise. In particular, it illustrates reasoning about the least element of a set. So here we go.
11 Jan 2023 » Memories: artificial intelligence at Stanford in the 70s
These days, artificial intelligence (AI) is synonymous with neural networks and machine learning (ML), but old-timers can remember when symbolic approachs were king: we now have the wonderful acronym GOFAI. I was at Stanford University from 1977 until 1982 and can vividly recall the unique atmosphere of the Stanford Artificial Intelligence Laboratory.
04 Jan 2023 » Mike Gordon and hardware verification
In the late 1960s, breakthrough papers by Robert W Floyd and Tony Hoare seemed to herald the advent of fully-verified software. Progress soon slowed however. It became clear that once you went beyond a simple flowchart program and had to deal with the horrors of procedures, variable scopes and aliasing, things were not so simple after all. I vividly recall, while still a student at Stanford, spotting a PhD dissertation boldly entitled Hardware Verification, and thinking that the author (Todd Wagner) had to be out of his mind to tackle something surely so difficult. Little did I suspect that I was soon to acquire a friend and colleague, Mike Gordon, who would make hardware verification a reality, and even make it look easy.
21 Dec 2022 » MetiTarski: an automatic prover for real-valued special functions
Way back when I first discussed interactive theorem proving with Mike Gordon, nearly 40 years ago, I wondered aloud whether we would ever see the formalisation of a really deep result in mathematics, such as the prime number theorem. It happened in 2004, when Jeremy Avigad formalised an elementary proof of the theorem (meaning, a proof not reliant on complex analysis) using Isabelle/HOL. (Paper also on ArXiv.) Jeremy remarked that he had spent an inordinate amount of time proving trivial inequalities involving the log function; he wrote a proposal on how such proofs might be automated, and eventually an implementation. I had my own ideas, and being lucky enough to live in an era when research grants could be awarded for crazy ideas, got funding to provide such automation as an extension to Isabelle/HOL. But things turned out differently and we ended up with a stand-alone automatic theorem prover, MetiTarski.
14 Dec 2022 » Thoughts on user interfaces for theorem provers
The era of the modern user interface can be dated from 1973, when the legendary Palo Alto Research Center (PARC) announced the Xerox Alto. Its unique combination of windows, icons, menus and a pointer (i.e. mouse) would eventually become ubiquitous. Suddenly everybody could master a computer, just as the rapidly shrinking cost of processors put one on everybody’s desk. When I joined the world of interactive theorem proving in 1982, there was much talk how verification would be easy if only implementors would adopt WIMP interfaces. Specific suggestions were made: above all, to let people select a subexpression and a rewrite rule in order to transform it. This is actually a dumb idea, since the computer can match rewrite rules to subexpressions automatically and apply them a thousand times per second. Verification is hard because specifications can be complex, formal proofs tend to be extremely long and the formalisation of intuitive mathematical ideas often requires great ingenuity. It’s not obvious what a mouse can do for you here. Forty years on, we have a clearer idea what a good user interface can do for verification, but the situation is by no means settled.
07 Dec 2022 » Memories: first exposure to computers
In The Life and Games of Mikhail Tal, the legendary former World Chess Champion mentioned his urge—when annotating his earliest games—to stretch out his hand to attach a question mark (indicating an error) to almost every move. That’s how I feel about my early experiments. I must have been about 15 when I first touched a computer keyboard, an ASR-33 teletype. Until then, my main hobby had been electronics: I built radios and owned a digital breadboard with a few flip-flops that could be wired together in different ways. I can’t remember which teacher pushed me in the direction of computers. Two others were involved: Mr Stanfield and Mr Hilbert. The latter taught Mathematics, but let’s be clear: I am not old enough to have met David Hilbert, and he was never a schoolteacher in the USA.
30 Nov 2022 » Martin-Löf type theory in Isabelle: examples
The previous post describes the implementation of Martin-Löf type theory in Isabelle. The ability to enter the rules in a notation as close as possible to the original papers and use them immediately for proofs was one of my key objectives for Isabelle in the 1980s. Now, through some tiny examples, let’s see how terms can be built incrementally with the help of schematic variables and higher-order unification. Such terms can be proof objects, but they do not have to be.
23 Nov 2022 » Martin-Löf type theory in Isabelle: formalisation
Last July, I described how Isabelle emerged from a jumble of influences: AUTOMATH, LCF and Martin-Löf. I stated that Isabelle had originated as a proof assistant for Martin-Löf type theory. Eventually I realised that the type theory community wasn’t interested in this work, just as it wasn’t much interested in Nuprl, which was by far the most developed type theory implementation out there. Both implementations had been left behind by the sudden change to intensional equality. As I mentioned in the earlier post, the type theory influence remains strong in the other formalisms supported by Isabelle, notably higher-order logic and ZF set theory. Few however may be aware that Isabelle’s instance for constructive type theory, Isabelle/CTT, still exists and still runs.
16 Nov 2022 » Automation and engineering in mathematics, by Pedro Sánchez Terraf
The interaction between Mathematics and Computer Science has grown deeper, even philosophically, with the use of proof assistants. The bonds made apparent by this connection highlight important lessons that we mathematicians have to learn from CS; and it is also important to discuss how different coding styles might help (or hinder) consolidating formalisation technology as a tool for the present and future generations of researchers and teachers of mathematics.
09 Nov 2022 » (Hilbert, Isabelle) and more universal pairs, by Marco David
Interest in formalizing the mathematics around Hilbert’s Tenth Problem was sparked almost simultaneously in Coq, Mizar, and Isabelle around five years ago. The problem, which demands an algorithm to decide the solvability of any Diophantine equation, is connected to a myriad problems in all fields of mathematics. For instance, the ABC and Goldbach conjectures as well as Fermat’s Last Theorem and the Four Color Theorem can be expressed in terms of Diophantine equations. The question posed by Hilbert is at the heart of the interface between computability theory and number theory.
02 Nov 2022 » Verifying cryptographic protocols, II: a simple example
Not long ago I wrote about cryptographic protocols and their verification. In this post, we shall see a simple example: the famous Needham-Schroeder public key protocol and its verification using Isabelle/HOL. The protocol will be the version as corrected by Lowe: the original provides weaker guarantees and is harder to reason about. Only highlights can be shown here. The proofs rely on a lot of formal machinery, which is described in the journal paper (also available here). For many people, crypto protocol verification rather than Isabelle seems to be my main research achievement, and yet they can’t really be separated: these techniques don’t seem to be reproducible in those proof assistants that have weaker automation, namely, all of them. I know that an attempt was made using a Certain Verification System.
26 Oct 2022 » Proving termination with multiset orderings
The title of this post is identical to the title of a seminal paper by Nachum Dershowitz and Zohar Manna, both of whom I knew as a graduate student at Stanford. (I had the privilege of doing directed reading under Zohar’s supervision.) Multisets are collections, like sets except that multiple occurrences of elements are significant. Computer scientists typically encounter them as a way of specifying the concept of sorting: to transform an input list into an output that is correctly ordered but equal to the input when both are regarded as multisets. Dershowitz and Manna showed that multisets also provided natural but strong orderings for proving termination. I had written about the termination of a rewrite system for Ackermann’s function in an earlier post and was advised to contact “Dershowitz, a leading expert on termination”. His reply was that the answer I sought was in his 1979 paper!
19 Oct 2022 » Verifying cryptographic protocols, I: Fundamentals
A cryptographic protocol is a message sequence, typically of fixed length, with the aim of establishing secure communications between two principals. On-line shopping is the application most people see: their computer will run a protocol (probably TLS) with the shopping site. TLS will authenticate the on-line shop to you (as assurance that you are not giving your credit card details to some impersonator) and encrypt your communications (keeping them secure from any eavesdropper). Viewed at a sufficiently high level, a protocol looks like an abstract program with the great advantage, to people like myself, of not ever having to think about nasty low-level things like bits. Although I have never verified code, I among many others have verified cryptographic protocols (also here). There is a lot of confusion about the basic ideas, which I hope to clarify below.
12 Oct 2022 » Verifying distributed systems with Isabelle/HOL, by Martin Kleppmann
We use distributed systems every day in the form of internet services. These systems are very useful, but also challenging to implement because networks are unpredictable. Whenever you send a message over the network, it is likely to arrive quite quickly, but it’s possible that it might be delayed for a long time, or never arrive, or arrive several times. When you send a request to another process and don’t receive a response, you have no idea what happened: was the request lost, or has the other process crashed, or was the response lost? Or maybe nothing was lost at all, but a message has simply been delayed and may yet arrive. There is no way of knowing what happened, because unreliable message-passing is the only way how processes can communicate.
05 Oct 2022 » Memories: Edinburgh ML to Standard ML
Dave MacQueen (with Robert Harper and John Reppy) has written a 100-page History of Standard ML. Here I offer my brief, personal and utterly subjective impressions of its early days, up to the deeply unfortunate schism that created what was then called Caml. Standard ML was a tragic missed opportunity. But even today there are still several viable implementations: Poly/ML, SML/NJ, Moscow ML and MLton. They are substantially compatible because the language was defined by an operational semantics. It’s sad that well into the 21st Century, Computer Science has so regressed that people no longer see the point of distinguishing between a programming language and its implementation.
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