Formalising an easy proof: Dirichlet's approximation theorem

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