For the holidays, some problems about prime divisors

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

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