by Jonathan Kujawa
Every institution has its founding myths. In mathematics, one of ours is that mathematical truths are unassailable, universal, and eternal. And that any intelligent being can discover and verify those same truths for themself.
This is why movie aliens who want to communicate with us usually use math [1]. The cornerstone of this myth is that mathematicians give airtight logical arguments for their truths. After all, Pythagoras knew his eponymous theorem 2500 years ago and it’s as true as it ever was. And it was equally true in Mesopotamia 3500 years ago and in China and India 2000+ years ago.
The idea of a “mathematical proof” is what makes math, math.
This semester I am teaching our introduction to mathematical proofs course. The not-so-secret purpose of the class is to help students transition from being mathematical computers to being mathematical creators. The students learn what it means to think mathematically. This includes how to take vague and ill-framed questions and turn them into mathematics, how to creatively solve those problems, and how to communicate those solutions in written and verbal form.
A huge part of the course is teaching the students what it means to give a valid proof. They learn about direct proofs (a direct logical march to the desired result), proofs by contradiction (if the desired result weren’t true, then one is forced to a logical impossibility), proofs by induction (using a recursive loop to verify the desired result), and more. They also learn some of the common pitfalls like pre-supposing the desired result and thereby begging the question.
The topics of the course are basic number theory, set theory, logic, functions, and the like, but the real content is how to read and write proofs.
As mid-metamorphosis mathematicians my students are starting to have a pretty good grasp of what makes a valid mathematical proof. They know to only use results whose proof they themselves have read with a critical eye and found convincing. They’ve mostly shed the prior version of themselves who would treat math as arbitrary facts brought down from the mountaintop on stone tablets. They are starting to feel pretty good about mathematics as a discipline and have bought the founding myth hook, line, and sinker.
There is an obvious problem. Mathematical proofs are written by humans and humans are fallible creatures. Even when we are careful and honest and self-skeptical, we can write down a “proof” that has a subtle gap or error. There are famous, infamous, and countless anonymous examples of proofs that have appeared in the literature and are now known to have errors.
The good news is that mathematics is a robust, anti-fragile system. The proof of Fermat’s Last Theorem by Andrew Wiles is an excellent example of this phenomenon. It was built on established results, traveled a path that should work if it could be pulled off, and established other important and interesting results as milestones along the way. When an error was found, these reasons made it seem likely the mistake could be corrected. It turned out to be much harder than expected but in the end the robustness of mathematics prevailed. Just as Wiles was about to admit defeat, he realized a combination of his earlier attempts could bridge the gap. Wiles and Richard Taylor were able to pull the strands together and finish the proof.
That said, every mathematician lives in quiet fear that one of their research papers will be torpedoed by the keen eye of an extra attentive graduate student. Every mathematician also knows of published work in their field which is known by experts to be fatally flawed [2].
Mathematics is slow to change, but it seems we are on the verge of a revolution. There are now proof verification software packages which are available. They are a bit like a spell and grammar checker, but for proof writing. As you write your proofs in these software packages, the computer dynamically checks for logical validity and alerts you to any mistakes you make.
Such software has been around for decades. Versions of this sort of verification software are used by companies like Microsoft, Toyota, and Airbus to verify the accuracy of their software. After all, you don’t want the computer of your car or plane to hit some unnoticed error while hurtling you along at maximum speed!
By and large, mathematicians have ignored the existence of this software. The main problem is that mathematicians are interested in doing interesting math. With some labor these software packages could be used to verify the validity of results that already have half a dozen different proofs, are undoubtedly true, and are taught to undergraduates. It was considered a significant step forward in 2012 when a group of researchers gave a formal computer verification of the odd order theorem. But this was first proven in the 1960s and it took six years to complete the verification. You’re not going to get mathematicians on board if it requires a lifetime of work to encode a bunch of well-known and classical results, just to verify the one result they actually care about.
In the past few years, proof verification software has become sophisticated enough to handle the tools of modern mathematical research. A good example of what is now possible is Lean. Lean is an open-source proof verification software package that was first developed by Leonardo de Moura at Microsoft Research nearly ten years ago.
Kevin Buzzard, a number theorist at the Imperial College London, has become the chief evangelist and driving force for bringing mathematics and mathematicians to Lean. Buzzard, his army of students and collaborators, and others have developed packages for Lean which includes big chunks of the undergraduate curriculum.
Contributors have also developed packages for manifolds, schemes, and perfectoid spaces [3]. These are serious mathematical gadgets that are of active interest to research mathematicians. Two of these are studied by colleagues in my department. You might convince them to use Lean if it already knows about some of their favorite things.
One can even imagine a near future where there is some level of AI involved which makes this software an actual Proof Assistant. One could imagine a mathematical dæmon that watches over your shoulder: pointing out mistakes but also suggesting potential strategies and relevant results [4]. If it can save even a fraction of the many hours I spend down pointless rabbit holes, dark dead-ends, and foolish pipedreams, then sign me up!
Relevant to my students, there is even an online proof-writing game built using Lean. It is called the Natural Number Game. Starting with the bare minimum of mathematics and proof techniques, you build up all the main characters in my intro to proofs course. For those of a certain personality, it’s downright addictive. Like most video games, it’s frustrating to the point of wanting to quit and then you start to make some real progress and it’s awfully hard to stop. For those of us who grew up playing Infocom text adventure games like the Hitchhiker’s Guide to the Galaxy it will feel awfully familiar [5].
The good news for math teachers is that spell and grammer checkers haven’t yet put composition teachers out of business. All the error checking and helpful suggestions in the world can’t replace the creativity of the human mind. Of course, when they solve the Millenium Prize Problems I will welcome our AI overlords :-).
[1] Of course if their motives are otherwise, then the aliens choose something more mysterious.
[2] This is another problem that could use solving. If you are a young researcher or an old researcher moving into a new area, you don’t know the folklore of the field. You don’t know the results “everybody” knows are true and haven’t bothered to write down, and you don’t know the published results which “everybody” knows are false. Worse, there are file drawers full of results and counterexamples and valuable data known only to the author. A huge amount of energy is wasted in scientific research by people rediscovering known lessons from the past. Of course, this duplication of effort also catches the oversights of previous generations, so it’s not all bad. One could even argue that part of the robustness of mathematics and the scientific process is this forced double-checking.
[3] Perfectoid spaces were only introduced ten years ago and are super hot and trendy in math these days.
[4] Or an exoskeleton for your mind.
[5] Fortunately, the Natural Number Game doesn’t have the wanton cruelty towards you, the player, that HGG does.