Many of you probably already know that this is true, from your own negative experience. I know that I often felt as if I was missing a lot of context when I was reading proofs in the abstract algebra book we used in grad school! How are these proofs validated? By other mathematicians reading them and accepting them as valid. The best known and most important proofs have been read and understood by many mathematicians, so we can trust that they are probably correct. If there were something wrong with the result, someone would have found out by now -- either by by finding an error in the proof or by discovering that something else breaks when we rely on it. Programmers know that this is how most programs are "proven" correct: by using them reliably for a long time under many different conditions. One problem with this process is that some proofs are so long and so complicated that the number of people who can read and understand them is quite small. For the results that break the most new ground, even the best mathematicians have to learn a lot to understand the proof. These "proof assistants" may not have the time, energy, or attention span to validate a result well enough that we "know" it is correct. A formal proof is an attempt to bypass the social process of mathematicians reading a result, providing the necessary context, filling in the details, and approving the result by automating those steps:Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader.

A formal proof will be less intuitive to most human readers, especially the advanced ones, but it should beA formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine.

The "kernel" of the system is small enough to be amenable to validation in several ways. One is the social process used for other programs: make the code open source and let everyone and his brother study it and use it. I love the way Hales embraces this approach:The computer code that implements the axioms and rules of inference is referred to as the kernel of the system. It takes fewer than 500 lines of computer code to implement the kernel of HOL Light [a particular computer proof assistant]. (By contrast, a Linux distribution contains approximately 283 million lines of computer code.)

(The emphasis is mine. More on that later.) This replaces the social process for validating proofs, up one level. Even if we validate the proof assistant only informally, it will be used repeatedly to validate proofs, and every use is an opportunity to find errors in the program. We can even use the program to validate proofs we already understand well just for the purpose of validating the program. (The world of mathematics is full of test data!) We use a social process to build a tool which then serves us over and over. Building tools is an essence of computer science. Given the small size of the program, we could also use formal methods to prove its correctness or at least offer evidence that it is correct. John Harrison used HOL Light to something akin to a formal proof of its own soundness. This is the first time in a long while that I have read about Gödel's incompleteness theorem coming into play with a real program... This approach made me think of the compiler-writing technique known as bootstrapping, though that's not quite what Harrison did. Finally, we might try to validate the program using another proof assistant. Hales calls this "exporting" a proof. The idea is this. Translate a proof written for one assistant into the language of another.I wish to see a poster of the lines of the kernel, to be taught in undergraduate courses, and published throughout the world, as the bedrock of mathematics.It is math commenced afresh as executable code.

For some reason, this reminded of cross-compilation, where we use a compiler on one platform to generate code for another platform. The purpose of cross compiling is to propagate programs onto systems where they do not exist yet. The purpose of exporting is different, to increase our confidence in one or both proof assistants. When we combine the confidence we have in the program via social acceptance with the confidence we gain from validating exported proofs, we have even more reason to trust the program, and thus the proofs it validates. Our confidence grows. This process reminds us all that math, while not a natural science, is imbued with the spirit of science:If a proof in one system is incorrect because of an underlying flaw in the theorem-proving program itself, then the export to a different system fails, and the underlying flaw is exposed.

We never know our proofs are correct. We only have good reason to believe so. The same is true of programs. That's another reason for a computer scientist like me to be fascinated by this direction in mathematics. The connection to the topic of the SECANT workshop is strong. Computing is helping to revolutionize how mathematicians work, just as it is revolutionizing how scientists work. Part of the math revolution will resemble the one in science, because some math research is itself inherently computational. The changes we talk about with formal proofs are a bit different, in that they are about how we validate results, not how we create them. Both traditional mathematics and computational mathematics depend ultimately on validation. Formal proof is aimed at addressing the former, but what of the latter? Certainly some scientists have recognized the problem and embarked on efforts to solve it. I wrote about one such effort early this year, a simulation-and-documentation system that interleaves programs, their execution, and the papers written to publish the results. Not surprisingly, such thinking and the systems that implement it require a change in mindset, one that will likely come only after a long... social process. Hales recognizes what the use of computing to generate and check proofs means for his discipline:With a computer -- indeed with any physical artifact, whether a codex, transistor, or a flash drive made of proteins from salt-marsh bacteria -- it is never a matter of achieving philosophical certainty. It is a scientific knowledge of the regularity of nature and human technology, akin to the scientific evidence that Planck's constant lies reliably within its experimental range. Technology can push the probability of a false certification ever closer to zero: 10^{-6}, 10^{-9}, 10^{-12}, ....