Where and how did computers help prove a theorem?

Question

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

Answer 1

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

Answer 2

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.

Answer 3

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

Answer 4

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!

Answer 5

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.

Answer 6

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.

Answer 7

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.

Answer 8

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.

Answer 9

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

Answer 10

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

Answer 11

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.

Answer 12

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

Answer 13

The formula for the Bailey-Borwein-Plouffe algorithm to compute the nth bit of Pi without computing any of the more significant bits was discovered, according to Simon Plouffe, using computer proof systems.

Answer 14

There are numerous examples in the average-case analysis of algorithms. Maybe some of the earliest are the computer experiments which led to the paper "Some unexpected expected behavior results for bin packing" by Bentley, Johnson, Leighton, McGeoch and McGeoch in STOC 1984.