Mathematics & Proof
Over thousands of years of our history, we humans have discovered many diverse, interesting, and sometimes useful, mathematical truths. We've done it through hard work, intuition, accident, or in some cases, mystical inspiration. Examples of such truths are the infinitude of prime numbers, the irrationality of $\sqrt{2}$, and the need for no more than four colours to colour a geographic map.
Alongside that is a second monumental achievement, the development of a system by which we convince ourselves, and each other, that these truths are actually true.
That system of proofs consists of commonly agreed fundamental axioms, and a rigorous framework of logic by which we progress an argument, step by step, from its beginnngs to a desired conclusion. Without such a framework, we would always be in doubt about the actual truth. Worse, we'd risk building further mathematics, false mathematics, on false foundations.
Without proof, our proposals remain conjectures. We may believe them to be true for personal reasons. We may believe them to be true by weight of experimental evidence. But all of that fails to meet the standard we set ourselves in mathematics. We must demonstrate that something is true using that framework of axioms and logic such that anyone else who agrees on the axioms and that logic, can't disgree with our conclusion. The only way they could disagree is to find a fault in the logic of our argument.
The discipline of proof, therefore, is a central pillar of mathematics.
And it is an eternal shame that most students aren't exposed to the idea of proofs at school, only encountering them if they choose to study mathematics at university.
Proof Assistants
Recent years have seen the emergence of software tools that aid the development or validation of proofs. Some tools produce strategies for proof, or even candidates for proofs.
Some tools, like Lean, focus on validating a proof that we write. Automatically checking a proof is a very powerful capability to have.
Installing and Running Lean
You can use the web-based version of Lean which only requires a modern web browser and internet access. There is nothing to install. This would be the idea solution for this first steps course of small proofs, but this service is new and sometimes fails requiring a refresh. Even so, everything in this course has been tested with this online service.
Many people have coalesced around using Microsoft's Visual Studio Code with the Lean extension which provides a richer environment. The extension installs everything you need to run Lean automatically. VSC is freely available for Linux, MacOS and Windows. The instructions at the following link will get you set up.
GitHub
All the code in this course is freely available online:
