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

Welcome to Software Cornwall’s event calendar, here you can find out about upcoming educational, networking and conference events being run by our members and the local tech community.

Loading Events

« All Events

  • This event has passed.

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

Thursday 12 08 2021 @ 5:00 pm - 6:00 pm

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!


More about: James Arthur,


Read a bit more about LEAN proof assistant:

* LEAN, an interactive theorem prover.
* The future of mathematics?
* A review of the LEAN theorem prover:


Practical stuff:

Due to the pandemic, this session will be online. A zoom link will be provided.

There is no cost to join the group and attend this event.

We write up all our events at our blog, which also links to code, references, slides and a YouTube video if recorded.


Join Zoom Meeting

Meeting ID:[masked]


Thursday 12 08 2021
5:00 pm - 6:00 pm


Online event


Data Science Cornwall