The concept of proof within the context of machine mathematics
[philosophy Hao Wang NG de Bruijn This post is prompted by a preprint, Automated Mathematics and the Reconfiguration of Proof and Labor, recently uploaded by Rodrigo Ochigame. It begins by contrasting two opposing ideals of proof — what any computer scientist would call top-down versus bottom-up – and then asks how they might have to be modified in a possible future in which mathematics is automated. To my way of thinking, his outlook is too negative.
The ideals of proof
The two ideals, which Ochigame are tributes to Ian Hacking, are as follows:
- Cartesian ideal of proof: “after some reflection and study, one totally understands the proof, and can get it in one’s mind ‘all at once’”
- Leibnizian ideal of proof: “every step is meticulously laid out, and can be checked, line by line, in a mechanical way”
I feel divided, because I seldom feel capable of understanding a proof all at once, and yet, having instead checked a lengthy proof line by line and getting to QED, I feel no more enlightened than before. Perhaps many people feel this way, and look for some compromise where they have a good idea about the mathematical tools that were deployed in the proof, and just to be careful, meticulously verify certain tricky or suspect calculations.
Ochigame himself explores a number of variations of these ideals in order to take into account modern day complications such as phenomenally long, complex or specialised proofs. He then outlines the history of the mechanisation of mathematical proof, beginning with AUTOMATH and Mizar, and concluding with today’s systems, such as Lean and Isabelle. Regarding these as proof checkers (where we are “verifying existing results”), he then briefly outlines the history of automated theorem proving, beginning with the work of Newell and Simon and mentioning Hao Wang. And now I feel obliged to mention again that while Newell and Simon got all the glory as AI pioneers, Wang’s system was on another planet when it came to capability. That’s because Wang actually understood logic. The AI world has often been driven by motives quite different from the actual competence of a particular AI system (see also SHRDLU: the importance of having a demo).
The role of computer-encoded proofs
Since most theorem provers work by reducing every claim to a string of low-level inferences in some built-in calculus, and since they don’t understand anything, we expect them to be firmly on the Leibnizian side. Ochigame proposes the following
- Practical standard of computer-encoded proofs: every step can be checked by a computer program and derived from the axiomatic foundations of the program; and after some study, one understands or trusts the encoding of the proven statement.
This formulation is natural enough, but I can imagine that mathematicians would be dissatisfied: it gives them no way to survey the proof themselves. They are forced to trust the computer program, its axiomatic foundations and even the underlying hardware, and realistically, they are going to have to trust the encoding of the proven statement as well.
Isabelle has supported legibility since Makarius Wenzel introduced his Isar structured language in 1999. Through this blog I have published numerous examples to demonstrate how much legibility you can obtain if you try. Too often, people don’t try. Incidentally, there is nothing about Isar inherently specific to Isabelle/HOL: it works for all of Isabelle’s incarnations, and I believe it could be adopted by Lean or Coq without modifying the underlying formalism. The chief difficulty is that a more sophisticated user interface would be required; an Isar proof is not simply a series of tactic invocations.
My ALEXANDRIA colleagues and I have formalised an enormous amount of advanced mathematics, but we were never satisfied with formalisation alone; we wanted our proofs to be legible. A mathematician still has to learn the Isabelle notation, but then should be able to read the proof without the aid of a computer. With existing automation, the computer seldom sees further than a mathematician, rather the opposite: we have to spell out many things that a mathematician would find obvious. At the moment, the chief exceptions are lengthy calculations and occasionally, large case analyses. If the time ever came that automation could find truly deep proofs, we would have to insist that it delivered intelligible justifications.
The future of formalised mathematics
Ochigame presents a bleak future in which formalisation becomes obligatory for mathematicians, with formalisers distinct from the mathematicians themselves and forming an underclass. The military origins of formal verification are also mentioned, in a vaguely ominous way.
I see the future differently. As proof assistants become more useful, and as more mathematicians become aware of them, their use will grow organically. Journals may eventually start to request formalisations of some material, but it’s likely that there will always be mathematics not easily formalisable in any existing system.
And another thing: why is it always about proofs?
Mathematics is too often presented as a discipline in which axioms are laid down and theorems proved from them. Sometimes, axioms are even conflated with beliefs, but I’m not going there today. Instead I would like to remark (as I have done before) the genius in mathematics typically lies in the definitions, not in the proofs. For example, Szemerédi’s regularity lemma is a straightforward proof — some calculations and an induction — relying on an extraordinary string of definitions. Why should we care about edge density? How did he come up with ε-regular pairs of sets, ε-regular partitions, the energy of a partition? How did he come up with the theorem statement? His genius was grasping the importance of these concepts.
The central importance of definitions like these gives something of a pass to those proof assistants (most of them) that don’t support legible proofs: if the definitions are there, you must be on the right track.
Postscript
I have a distant memory of NG de Bruijn (visiting Caltech in 1977) describing the “mathematics assembly-line”. He wrote down the word Genius, then an arrow pointing to “first-rate mathematician”, then I believe a further arrow pointing to “student”, a further arrow pointing to “journal” and there he drew a little tombstone. To my mind this conjures up the genius who has the ideas and the junior colleagues who fill in the details to make the work publishable. (And yet, he himself seems to have published almost exclusively as sole author.) Conceivably, formalisation will begin to play some role on the journey from the genius to the grave.