Mechanizing Proof: Computing, Risk, and Trust

Professional mathematicians typically never argue about the methods of proof that they use, although they argue quite frequently whether a collection of statements does indeed constitute a proof. The development of a proof can take years in some cases, but the discovery of an error in a proof involves relatively short scales of time. The proofs that mathematicians subject to peer review are a mixture of natural language and mathematical symbolism, but the deductive nature of the steps in the proof are readily apparent, and the mathematical community has deemed this style of mathematical scholarship acceptable. This informal structuring of a mathematical proof is to be contrasted with that insisted upon by logicians, who insist that a proof should be a listing of formal statements, with each being a deduction from prior ones. If natural language appears it is only as metamathematical commentary and is set apart from the proof itself. These proofs are thus difficult for a human to read, unless they have in-depth knowledge and experience of the formalism that is used. This style of (formal) proof has been followed by those involved in research in automated theorem proving or in the very important field of formal verification. The discovery of a new proof of an old mathematical result or the discovery of new concepts in mathematics by a machine is the goal of this research, and it has had varying degrees of success in the last few decades.If an error were discovered in one or more of the many mathematical results that exist in the literature, it would bring no risk to human society in general. These results are usually highly esoteric, and have no practical application, so any error discovered in them would probably only cause pain to the mathematician(s) responsible for them. However, computer scientists have realized that huge software programs that are critical to business, industry, and government are efficiently analyzed in the framework of certain mathematical structures. The flow of the program can be viewed as a deduction, in a manner very similar to what goes on in proofs of mathematical results. It is essential that these programs are without error (or "bugs"), and thus error-checking becomes proof-checking in this approach. This brings up of course the question as to whether these proof-checkers are themselves free of error. Who is to decide whether a sequence of statements, be they a software program or a series of formal deductions, do not contain errors?This question, along with many other highly interesting topics, is discussed in this book. It could be read by anyone interested in automated theorem proving, formal verification, automated mathematical discovery, natural language processing, and artificial intelligence. The author has done an excellent job of articulating on the nature of proof, both formal and informal, and the risks involved in trusting machines to verify the reliability of both hardware and software. The latter is the main issue in the field of formal verification, and is one that is of immense importance in the modern world, whose technological complexity is increasing hyper-exponentially. It is because the machines and technology of today are so complex that one needs an effective methodology for checking their design and functioning to ensure that they are not flawed to a degree that may cause death or needless suffering to human beings. Can we trust a machine to check the design of medical equipment or do a verification of software? What if the machine makes a mistake or is itself the result of a faulty design? And for highly complex equipment or software, will the results of the machine check be comprehensible to a human?The author outlines the history of proof theory, proof checking, and formal deduction, and includes anecdotal discussion of some of the researchers in these areas. For this reviewer, the most interesting part of the book was the last two chapters, for it is here that the author discusses the societal impact of machine proof. One learns for example that some of the early implementations of machine proof allowed a substantial amount of "hints" from the human user. This is not really surprising, since early developments in artificial intelligence can be characterized by the need for inputs from a human tutor. The goal of course is to free the machine from the need for this tutoring, and become essentially independent, to "think for itself". The author clearly believes that this presents a danger, and he points to the need for continued interactions between the machine and society in order that decision-making is carried out safely and in a way that is productive to human society as a whole. He believes that treating proving machines as "oracles" is dangerous, but he realizes that these kinds of machines have become a "permanent part" of our culture.The author's anxiety is somewhat unjustified if one takes cognizance of the fact that the use of these kinds of machines is due to the efforts of human researchers, who have a thorough understanding of their functioning and limitations. And these machines are not autonomous. Their skill and efforts in proof checking, theorem proving, or formal verification is due solely to the instigation of a human investigator. But his anxiety is justified if judged relative to future developments. With each passing day, we place more of our trust in these types of machines, among many others, who are now responsible for financial decision-making, drug discovery, network management, legal casework, and myriads of other socially beneficial functions. It is becoming more rare to discover that these machines have made a mistake, but it is also becoming rarer for humans to take the initiative to find any mistakes. As machines are designed to become more autonomous they will themselves take the initiative to engage in activities that may or may not be deemed useful to human societies. The degree of symbiosis between the human and machine communities will therefore be directly proportional to their mutual trust.