I felt like I wasn’t living up to this blog’s name, so here’s a manifesto about mathematics, something about which I know very little.

We should engineer mathematics. We must treat mathematics as an engineering discipline. The process of doing math should be the process of writing code.

Mathematics is reaching fundamental limitations with its current techniques and tools. Proofs are exceeding the capacity of a single mind. Verifying arguments is becoming nigh impossible. The core value of rigor is at stake here.

There is some irony here. Engineering itself was made rigorous through mathematics. Now it must give the rigor back to mathematics.

I say “should” and “must”, but really these judgements are irrelevant. Mathematics will become a field of engineering. The tools of engineering will not only return mathematics to rigor, but they will offer their users immense freedom and fun in their use. Future generations will adopt these tools with such fervor that they will not comprehend practicing math without them.

Proof checking is the beginning of this reinvigoration. The art of writing manual proofs will be seen by future generations like dictation—quaint exercises from a byegone era.

Of course that is not a surprise. Mathematics has been stuck in antiquated techniques for ages. Professors write on chalkboards while doctoral programs continue to give oral exams. Not all of the old is bad, but all should be reassessed perpetually.

The act of hand writing a proof, while it holds some charm and sentimental value, will ultimately not be mourned when it passes on. The hand written proof offers no feedback, no systematic format to parse, no way of partitioning beyond chapters or lemmas.

Mathematicians scorn contributions from outside the world of academia, treating the authors as crackpots, without reflecting that they have no choice but to be crackpots, as there is no way to learn the art of rigor without entering the temple of the math course and submitting one’s self to the lashings of grading. With proof checking, perhaps we will see a swell of self-taught mathematicians, a democratization of the field.

Even in the temple itself, we will see a shift. As of now, undergraduates mathematics majors must learn the praxis of proofs through repeated, thorough and unforgiving feedback from either a professor or a teaching assistant. This requires endless hours of grading flawed proofs, some flawed in obvious manners but perhaps some in less clear ways. If a professor neglects this duty and lets students through with flawed proofs, the damage is severe. Undergraduates leave without understanding the core essence of proof and simply the ritualistic aspects, the stitled vocabulary and standard phrases.

Instead let us imagine a course where undergraduates are to use a proof checker. If they attempt to construct an incorrect proof, whether broadly or subtly incorrect, the checker will spit it back with direct, specific feedback. Unlike the feedback of the hand written proof, where the work and therefore the grade is a fait accompli, the feedback of a checker offers opportunities to improve, to tweak, to play. Play is the essence here. Mathematics offers immense opportunities to play, but the mathematician must be both player and referee. They must guard their thoughts without certainty that they are correct. With a proof checker, they can play, knowing the proof checker is keeping them in line.

However proof checking is only the beginning. Once math is represented in code, it will be natural that mathematicians will begin adopting the standard operating techniques of software engineers. Yes, rare is the mathematician who adopts these techniques in the programs currently written by mathematicians such as numerical simulations. But a numerical simulation is not the fundamental core of the mathematician’s work. It is merely an offshoot, a representation of the work.

Furthermore, the mathematician of now will be different than the mathematician of future generations. As mathematics starts to be coded instead of written, the field will attract coders. We often assume that if one likes a field, one would like it in any time period, but that is incorrect. The physics of the 20th century is unrecognizable to the physics of the 18th century. The mathematics of the 22nd century may be unrecognizable to us.

And finally it will be those who use the tool to its utmost, who learn to scale programs using software development techniques, those will be the ones who make progress and who people will follow.

We can imagine a mathematics research group of the future. Mathematicians will work on programs, each member given a specific portion to write, whether that is a theorem or a preliminary lemma. While proof checkers should guarantee correctness, inevitably some parts of the code will require tests to counterbalance holes in proofs or potential bugs. Undergraduates or even non-students will be able to contribute as long as their code compiles and passes tests. When a theorem is completed, the group can publish its code on a package repository, where other groups can download the code and use it in their proofs. The group will consider the best interface and abstractions to make their code usable for other groups.

This should sound revolutionary to a mathematician and utterly mundane to a programmer. And indeed the mathematicians mentioned will not be those who are currently working, or even those who are in school. They will be a generation who is brought up in these techniques, who thinks about math in code. It is now our job to bring about this generation.