Proof, Provers, and the Lean Theorem Prover - Summer Special!

In this summer special we'll take a break from messy data, and - just for fun - take refuge in the reassuring consistency and cleanliness of logic and mathematics, by exploring automated theorem provers and proof assistants.

We're very lucky to have the very friendly and enthusiastic Cornwall-based James Arthur, a pure mathematician and mathematics communicator, give us a talk covering:

• What is a proof, anyway?
• What is a theorem prover, what is a proof assistant?
• Introduction to the LEAN prover.
• Simple worked example of a proof with LEAN.

This event is aimed at beginners who are not necessarily experts in mathematics or proofs. The aim is to inspire you to find out more and have a go yourself!