Lab Lunch: 5 February 2019 - Paul Jackson

Title: Lean - a new Interactive Theorem Proving System


Interactive theorem provers help users formalise, check and automate proofs in pure and applied mathematics, programming language semantics, and the formal verification of software and computer hardware.  They find application in education, academic research and industry.

Up to recently the interactive theorem proving landscape has been dominated by mature tools (e.g. Coq, Agda, HOL4, HOL-Light, Isabelle/HOL, PVS, ACL2) that each has been developed over 25-30 years or more.  The large amount of work needed to produce new competitive tools has dissuaded most from investing the effort.  4 years ago a new system Lean ( was introduced, a co-production initially of Microsoft Research and CMU.  Over the last 2 years it has attracted a suprisingly large and enthusiastic cohort of users.

A few weeks ago I attended an informal 5-day meeting for the Lean community (  25 were expected.  Over 60 turned up, including 29 who describe themselves as mathematicians.  In this talk I’ll report on the meeting, trying to identify why Lean has had the success it has so far and discussing where it might be going.

I’ll aim to keep the talk at a high level.  No familiarity with interactive theorem proving or dependent type theory (the kind of mathematical foundation Lean uses) will be assumed.

Feb 05 2019 -

Lab Lunch: 5 February 2019 - Paul Jackson

Speaker: Paul Jackson

MF2 level 4