# Where and how did computers help prove a theorem?

The purposes of this question is to collect examples from theoretical computer science where the systematic use of computers was helpful

1. in building a conjecture that lead to a theorem,
2. falsifying a conjecture or proof approach,
3. constructing/verifying (parts of) a proof.

If you have a specific example, please describe how it was done. Perhaps this will help others use computers more effectively in their daily research (which still seems to be a fairly uncommon practice in TCS as of today).

(Flagged as community wiki, since there is no single "correct" answer.)

-
I should say I'm particularly interested in instances of (1) and (2). That is, cases where computers helped shape human intuition in crucial ways. –  Moritz Aug 18 '10 at 16:03
Some of the more recent answers to this question, at the end of the list, are excellent and worth reading. I suggest reading to the end! –  András Salamon Nov 8 '10 at 15:14
fyi similar to mathoverflow, Interesting conjectures “discovered” by computers and proved by humans? –  vzn Sep 20 '12 at 17:21

A very well-known example is the Four Color Theorem, originally proven by exhaustive checking.

-
(Arguably) not theoretical computer science. –  JɛﬀE Aug 17 '10 at 21:16

Fix $n$ points in the plane. Let T be a triangulation (i.e a planar straight-line graph with the points as vertices that is fully triangulated), and let the weight of the triangulation be the sum of the edge lengths.

Showing that the minimum weight triangulation (MWT) problem was NP-hard was a long standing open problem, made difficult by the fact that edge lengths involve square roots, and the desired precision needed to compute these accurately was difficult to bound.

Mulzer and Rote showed that MWT was NP-hard, and in the process used computer assistance to verify the correctness of their gadgets. As far as I know, there is no alternate proof.

-

Thomas Hales proof (his site, MathSciNet) of the Kepler conjecture involved so much case analysis -- and the cases were in turn verified by computer -- that he decided to attempt a formal proof of it. His project to do so is FlysPecK, and he estimates it will take 20 years of work.

Researchers in Programming Languages regularly use computer-aided proofs in their work, though I do not know how essential this is in terms of their research process (it certainly keeps them from having to write out tons of tedious manipulations, though).

-

Computers have been also used to determine upper bounds on the running times of backtracking programs solving NP-hard problems, and construct gadgets to prove inapproximability results. This and other fun-filled topics await you in a short essay (warning, extreme self-promotion ahead) entitled "Applying Practice To Theory." See http://arxiv.org/abs/0811.1305

Given this nice list, it looks like I should update the paper!

-
That's a very nice survey. Thanks. –  Moritz Aug 19 '10 at 4:31
Yeah, I like it too. –  Daniel Apon Aug 19 '10 at 4:45

Doron Zeilberger has done some work in the field of computer-generated proofs. Most notably, he has prepared a Maple program to prove geometric identities, and another program to prove a class of combinatorial identities. Some of the methods are mentioned in the book A=B.

-

A counterexample to the Hirsch conjecture, important to linear programming and polyhedral combinatorics, was proposed by Francisco Santos very recently. Computer verification was used first to establish some of the properties required of the example, although arguments without the assistance of computational power were discovered afterwards, cf. Gil Kalai's blog post or the paper on arxiv.

-

The Karloff–Zwick algorithm for MAX-3SAT achieves expected performance 7/8. However the analysis relies on unproven spherical volume inequalities. These inequalities were finally confirmed via computer assisted proofs in Zwick's another paper.

Besides Hales' proof to the Kepler conjecture as mentioned above, the proof to the Honeycomb conjecture and the one to the Dodecahedral conjecture are computer aided as well.

-
While we're in this vein, Weaire and Phelan's disproof of the Kelvin conjecture was also computer-aided. (en.wikipedia.org/wiki/Weaire%E2%80%93Phelan_structure) –  Peter Shor Nov 9 '10 at 15:49

Haven't seen this mentioned here, but an automated theorem prover solved the long standing open problem of whether Robbins algebras are boolean:

http://www.cs.unm.edu/~mccune/papers/robbins/

This is especially notable because the computer developed the entire proof and the problem had been open for several decades.

Not completely sure if it qualifies as TCS, but arguably it is closely related.

-
An answer mentioning this was posted in mid-August, but the answer was deleted by the owner in late September. It is a nice example. –  András Salamon Nov 8 '10 at 15:18

You can check out Shalosh B. Ekhad's homepage. This computer has been publishing papers for a while (usually with coauthors).

-

The results in "The Geometry of Binary Search Trees" by Demaine, Harmon, Iacono, Kane, and Patraşcu were developed with the help of software to test various charging schemes and construct optimal asses for small access sequences. (And yes, "asses" is the correct term.)

-
By "asses" I assume you mean "Arborally Satisfied Sets"? Maybe I have given away the fun of the acronym. :) –  Andrew W. Aug 17 '10 at 22:58

N. Shankar verified (fully and mechanically) Godel's proof of the incompleteness theorem and the Church--Rosser theorem using the Boyer--Moore theorem prover. There is a book describing how it was done.

-

Christian Urban used the Isabelle proof assistant to check one of the main theorems in his PhD thesis was actually a theorem [1]. Using the assistant, a few changes needed to be made, but the result pretty much stood up.

Similarly, Urban and Narboux also discovered errors in a pen and paper proof of Crary's completeness proof for equivalence checking.

Meikle and Fleuriot formalised Hilbert's Grundlagen in Isabelle and demonstrated that, contrary to Hilbert's claims, he was still relying on his intutition to formalise geometry in an axiomatic manner (IIRC there were holes in his proof derived from Hilbert assuming things about diagrams) [3].

[1]: Revisiting Cut-Elimination: One Difficult Proof is Really a Proof

[2]: Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking

[3]: Formalising Hilbert's Grundlagen in Isabelle/Isar

-