Computing huge Fibonacci numbers, by proof and by code

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

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