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
- 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.