How well accepted are proofs where critical parts depend on software of which we have no access to the source, e.g Mathematica, Maple?

More generally how much can we take on faith with regards to software. Do we have to check the compiler for the Four Color Theorem?

  • 4
    $\begingroup$ Four color theorem became more accepted after Seymore/Robertson got an independent (also computer assistent) proof of it. Later, Seymore/Robertson provided a 500 page long proof of graph minor theorem. Verifying correctness of a computer generated proof might be easier than 500 page long "traditional" proof. $\endgroup$ Jan 18 '11 at 2:28
  • 3
    $\begingroup$ There's a computer-verified proof of the four color theorem. That means that the computer produced a proof in some formalism (something like predicate logic but different). That's a degree of certainty which is far superior to most "human" proofs, which often contain errors. $\endgroup$ Jan 18 '11 at 3:39

A few years ago the Notices of the American Mathematical Society ran a series of articles on the state of the art in using computer proof assistants. They are at least worth skimming.

  1. "Formal Proof," by Thomas Hales

  2. "Formal Proof - The Four-Color Theorem," by Georges Gonthier

  3. "Formal Proof - Theory and Practice," by John Harrison

  4. "Formal Proof - Getting Started," by Freek Wiedijk

I tend to be a traditionalist when it comes to traditional methods versus computer methods, but I do find arguments like the following compelling.

(This is from a news release from the AMS on their series of articles on formal proof.)

"When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible." [emphasis mine]

(And this is from Hales's article.)

"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."

Verifying correctness on such a small program would be a lot easier than verifying correctness of proofs of many theorems.

(Also from Hales's article.)

"Experience from other top-tier theorem-proving systems has been that about three to five bugs have been found in each system over a period of 15-20 years of use. After decades of use on many different systems, to my knowledge, only one proof has ever had to be retracted as a result of a bug in a theorem-proving system, and this in a system that I do not rank in the top tier... We can assert with utmost confidence that the error rates of top-tier theorem proving systems are orders of magnitude lower than error rates in the most prestigious mathematical journals." [emphasis mine again]

As a side note, Hales's paper also lists several major theorems (already proved the traditional way, of course) that have been since proved by a computer. These include quadratic reciprocity, the prime number theorem, the fundamental theorems of algebra and calculus, the Jordan curve theorem, and the Brouwer fixed-point theorem.

Besides the Four-Color Theorem, apparently the Robbins conjecture was first proved by an automated theorem prover.

And, of course, there's Wikipedia on computer-assisted proof.


Many of your questions are adressed in this new book of Jon Borwein and Keith Devlin:



I'd argue for a mixed proof system. Computer proofs should be more accepted that they are now, but the tradition is slow to build. I'd rather trust a proof that has also been checked by a computer, in addition to traditional peer-review. After all, there is only so much amount of abstraction that a human brain can handle, and at times small details can change everything. As Alain Connes put it in the Princeton Companion, the most difficult step in a mathematical work is checking for mistakes.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.