In this summer special we took a break from messy data, and - just for fun - took refuge in the reassuring consistency and cleanliness of logic and mathematics, by exploring proofs and proof assistants like LEAN.
We were very lucky to have James Arthur, a Cornwall based pure mathematician and mathematics communicator, give an introduction to proofs and the LEAN proof assistant, and a worked example.
The video for this talk is at our channel: [youtube]. Slides are here: [pdf or pdf].
What is a Proof Anyway?
James started by explaining that mathematics is different to science. Science starts with theories about how the world works, and tries to find evidence in support of those theories, until someone finds evidence that disproves or refines those theories.
Mathematics, on the other hand, is built on logical arguments, with truths leading to new truths solely by following a system of consistent logic. You can't argue with mathematical discoveries if you agree with the truths they were built on, and the logic of the argument that connects the two.
It is possible to work backwards to the very foundations on which branches of mathematics have grown - and find that you arrive at very fundamental simple statements that can't be decomposed further - these are the starting axioms of mathematics. Mathematicians will of course experiment to see where different axioms lead ... but that is a story for another day!
James went on to explain that lemmas are small, less important theories, and that both are traditionally structured as a statement and then a proof.
A proof can be deductive - simple statements leading to subsequent statements - but other strategies are possible. A common example is proof by contradiction, where a correct set of logical arguments leads to an evidently false conclusion which proves the starting assumptions were false, a surprisingly useful and common strategy. For example, proving $\sqrt(2)$ is irrational is done by contradiction (proof).
Another strategy is induction, which is slightly more sophisticated. If a natural number $n$ belongs to a set, and we know that at least one number like 0 does too, then if we can show that the successor $n+1$ also belongs to that set, then like falling dominoes, so do all numbers. What makes this useful is if the set itself is interesting. Let's phrase this a different way to make sure we understand it:
- If $\phi(0)$ is true,
- And we can show that $\phi(n)$ is true implies $\phi(n+1)$ is also true,
- Then by induction $\phi(n)$ is true for all natural numbers $n$.
You can follow a simple worked example (here).
What is a theorem prover, what is a proof assistant?
Developing proofs is not easy, and is a learned skill.
It is too easy to make errors in logic as we assert new facts from previous facts, or we make a mistake about completeness of coverage, or we incorrectly assume a statement about integers is true for real numbers, ... the ways in which we might have errors or gaps in our proofs is overwhelmingly large.
A proof assistant helps us write correct proofs by telling us when there is an error in the logic.
Although the terms are sometimes mixed, a proof assistant is different to a theorem prover which tries to find a proof that connects starting facts to a goal.
The development of a theorem prover, and indeed a theorem generator, has been a holy grail of computer science and mathematics since the early days of digital computing. Great advances have been made but the problem has not been universally solved.
The LEAN proof assistant is a relatively modern project, and has been enthusiastically embraced by mathematicians.
A unique element of LEAN is that it interactively shows you the state of a proof, including the state of sub-goals towards the overall proof goal. Watch James's example next to see this in action.
James's Worked Example: Area Of A Circle
James explained how LEAN proofs are written in a functional language, and proceeded to demonstrate with a live demonstration. Due to time constraints he didn't get the chance to complete it.
He did recommend a separate demonstration he did with LEAN to prove the area of a circle.
Further Reading
Read a bit more about LEAN proof assistant:
- Very first hands-on steps with LEAN: https://xenaproject.wordpress.com/2017/09/30/proving-trivial-things-with-lean/
- LEAN, an interactive theorem prover. http://leanprover.github.io
- Extensive tutorial and guide: https://leanprover.github.io/tutorial/tutorial.pdf
- 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/
- Natural Language Number Game: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
- James' video on proving the area of a circle with LEAN: https://youtu.be/DbiJD_jqe-g
- An accessible worked example proving a numerical summation relation: https://ahelwer.ca/post/2020-04-05-lean-assignment/
