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, https://uk.linkedin.com/in/jamesa9283

—-

Read a bit more about LEAN proof assistant:

* LEAN, an interactive theorem prover. http://leanprover.github.io
* The future of mathematics?
https://www.ma.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf
* A review of the LEAN theorem prover:
https://jiggerwit.wordpress.com/2018/09/18/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. http://datasciencecornwall.blogspot.com

—-

Join Zoom Meeting
https://us02web.zoom.us/j/89689662632?pwd=cDBGVWJBdnVVR09XdG12UGw0Z2kydz09

Meeting ID:[masked]
Passcode:[masked]