lawrencecpaulson.github.io

For many, the process of transforming a textbook mathematical proof into a formal document remains mysterious. Here, we look at a straightforward example. Dirichlet’s approximation theorem states that each real number has a rational approximation with a relatively small denominator. The proof combines an application of the pigeonhole principle...

One of the key tensions in theorem proving is between reasoning about things and using them in serious computations. One way to address this tension is through computational reflection: treating logical formulas as executable code, when you can. The first realisation of this idea was the Boyer/Moore theorem prover, which was initially created to...

Just in time for the holiday break, here are some small exercises to build your skills. The subject matter is the prime numbers: specifically, the maximum exponent of a prime divisor of a number. A skeleton Isabelle theory file is available, containing all statements of the theorems and necessary definitions or boilerplate, but no proofs. Your...

I am often asked, “how do I get started with Isabelle?” For example, why don’t we have an analogue of Kevin Buzzard’s excellent Natural Number Game for Lean? Well, maybe I am lazy, but it’s impossible to re-create the Isabelle experience in a web browser. Instead, we make it easy for you to install Isabelle on your own machine, be it Windows,...

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

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

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

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

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

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