Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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

share|improve this question
    
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
2  
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

14 Answers 14

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

share|improve this answer
6  
(Arguably) not theoretical computer science. –  JɛffE 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.

share|improve this answer

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

share|improve this answer

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!

share|improve this answer
    
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.

share|improve this answer

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.

share|improve this answer

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.

share|improve this answer
1  
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.

share|improve this answer
1  
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

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

share|improve this answer
1  
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

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

share|improve this answer

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.

share|improve this answer

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

share|improve this answer

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.

share|improve this answer

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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