Lab 23: The Lean Theorem Prover

From the Lean Theorem Prover community website:

A proof assistant is a piece of software that provides a language for defining objects, specifying properties of these objects, and proving that these specifications hold. The system checks that these proofs are correct down to their logical foundation.

These tools are often used to verify the correctness of programs. But they can also be used for abstract mathematics…. In a formalization, all definitions are precisely specified and all proofs are virtually guaranteed to be correct.

In this lab, we will get a sense of how a theorem prover works by proving basic properties of the natural numbers in the interactive theorem prover Lean. Visit

https://adam.math.hhu.de/#/g/leanprover-community/nng4

Start by reading the instructions on the left-hand side of the page, under “Welcome to the Natural Number Game.”

Task 1

Complete every level from each of the following worlds:

1. Tutorial World

2. Addition World

3. Multiplication World

4. Implication World

5. Advanced Addition World

6. Inequality World