<p>A very well-known example is the <a href="http://en.wikipedia.org/wiki/Four_color_theorem">Four Color Theorem</a>, originally proven by exhaustive checking.</p>

CC BY-SA 2.5
2010-08-17T21:16:58.723Z
(Arguably) not theoretical computer science.
Jeffε
CC BY-SA 2.5
2010-08-17T02:50:07.540Z
2010-08-17T02:50:07.540Z
Evgenij Thorstensen
<p>Doron Zeilberger has done some work in the field of computer-generated proofs. Most notably, he has prepared a Maple program to <a href="http://www.math.rutgers.edu/~zeilberg/GT.html">prove geometric identities</a>, and another program to prove a class of <a href="http://www.math.temple.edu/~akalu/html/pg1.html">combinatorial identities</a>. Some of the methods are mentioned in the book <a href="http://www.math.upenn.edu/~wilf/AeqB.html">A=B</a>.</p>

CC BY-SA 2.5
2010-08-17T10:24:27.277Z
2010-08-17T10:24:27.277Z
Tomer Vromen
<p>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 <em>(warning, extreme self-promotion ahead)</em> entitled "Applying Practice To Theory." See <a href="http://arxiv.org/abs/0811.1305">http://arxiv.org/abs/0811.1305</a></p>

<p>Given this nice list, it looks like I should update the paper!</p>

CC BY-SA 2.5
2010-08-19T04:45:30.437Z
Yeah, I like it too.
Daniel Apon
CC BY-SA 2.5
2010-08-19T03:29:00.723Z
2010-08-19T03:29:00.723Z
Ryan Williams
<p>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. </p>

<p>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. </p>

<p><a href="http://arxiv.org/abs/cs/0601002">Mulzer and Rote showed that MWT was NP-hard</a>, and in the process used computer assistance to verify the correctness of their gadgets. As far as I know, there is no alternate proof. </p>

CC BY-SA 2.5
2010-08-17T03:06:02.870Z
2010-08-17T03:06:02.870Z
Suresh Venkat
<p>Thomas Hales proof (his site, <a href="http://www.ams.org/mathscinet-getitem?mr=2179728">MathSciNet</a>) 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 <a href="http://code.google.com/p/flyspeck/">FlysPecK</a>, and he estimates it will take 20 years of work.</p>

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

CC BY-SA 2.5
2010-08-17T03:34:54.540Z
2010-08-17T03:34:54.540Z
Joshua Grochow
<p>A counterexample to the <a href="http://en.wikipedia.org/wiki/Hirsch_conjecture">Hirsch conjecture</a>, 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. <a href="http://gilkalai.wordpress.com/2010/06/15/a-counterexample-to-the-hirsch-conjecture-is-now-out/#comments">Gil Kalai's blog post</a> or the <a href="http://arxiv.org/abs/1006.2814">paper on arxiv</a>.</p>

CC BY-SA 2.5
2010-08-17T08:41:06.750Z
2010-08-17T08:41:06.750Z
RJK
<p>Haven't seen this mentioned here, but an automated theorem prover solved the long standing open problem of whether Robbins algebras are boolean:</p>

<p><a href="http://www.cs.unm.edu/~mccune/papers/robbins/">http://www.cs.unm.edu/~mccune/papers/robbins/</a></p>

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

<p>Not completely sure if it qualifies as TCS, but arguably it is closely related.</p>

CC BY-SA 2.5
2010-11-08T15:18:36.487Z
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
CC BY-SA 2.5
2010-11-08T03:45:32.857Z
2010-11-08T03:45:32.857Z
Mugizi Rwebangira
<p>The <a href="http://en.wikipedia.org/wiki/Karloff%E2%80%93Zwick_algorithm">Karloff–Zwick algorithm</a> 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 <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.3939">another paper</a>.  </p>

<p>Besides Hales' proof to the Kepler conjecture as mentioned above, the proof to the <a href="http://en.wikipedia.org/wiki/Honeycomb_conjecture">Honeycomb conjecture</a> and the one to the <a href="http://en.wikipedia.org/wiki/Dodecahedral_conjecture">Dodecahedral conjecture</a> are computer aided as well.</p>

CC BY-SA 2.5
2010-11-09T15:49:00.170Z
While we're in this vein, Weaire and Phelan's disproof of the Kelvin conjecture was also computer-aided. (http://en.wikipedia.org/wiki/Weaire%E2%80%93Phelan_structure)
Peter Shor 
CC BY-SA 2.5
2010-08-17T11:21:42.567Z
2010-08-17T12:56:04.430Z
2010-08-17T12:56:04.430Z
Zeyu
<p>You can check out Shalosh B. Ekhad's <a href="http://www.math.rutgers.edu/~zeilberg/ekhad/papers.html">homepage</a>.  This computer has been publishing papers for a while (usually with coauthors).</p>

CC BY-SA 2.5
2010-08-18T04:38:27.843Z
2010-08-18T04:38:27.843Z
Lev Reyzin
<p>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.</p>

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

<p>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].</p>

<p>[1]: Revisiting Cut-Elimination: One Difficult Proof is Really a Proof</p>

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

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

CC BY-SA 2.5
2010-08-23T20:51:22.127Z
2010-08-23T20:51:22.127Z
Dominic Mulligan
<p>N. Shankar <em>verified</em> (fully and mechanically) Godel's proof of the incompleteness theorem and the Church--Rosser theorem using the Boyer--Moore theorem prover. There is a <a href="http://rads.stackoverflow.com/amzn/click/0521585333">book</a> describing how it was done.</p>

CC BY-SA 2.5
2010-08-18T11:06:17.977Z
2010-08-18T11:06:17.977Z
Radu GRIGore
<p>The formula for the <a href="http://en.wikipedia.org/wiki/Bailey%E2%80%93Borwein%E2%80%93Plouffe_formula">Bailey-Borwein-Plouffe algorithm</a> to compute the nth bit of Pi without computing any of the more significant bits was discovered, <a href="http://groups.google.com/group/sci.math.symbolic/msg/5b7e62ce42ae0cb6?pli=1">according to Simon Plouffe</a>, using computer proof systems.</p>

CC BY-SA 2.5
2010-08-23T22:03:22.583Z
2010-08-23T22:03:22.583Z
Ross Snider
<p>The results in "<a href="http://www.siam.org/proceedings/soda/2009/SODA09_055_demainee.pdf">The Geometry of Binary Search Trees</a>" 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.)</p>

CC BY-SA 2.5
2010-08-17T22:58:46.323Z
By "asses" I assume you mean "Arborally Satisfied Sets"? Maybe I have given away the fun of the acronym. :)
Andrew W.
CC BY-SA 2.5
2010-08-17T21:19:19.503Z
2010-08-17T21:19:19.503Z
Jeffε
<p>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.</p>

CC BY-SA 2.5
2010-11-08T13:28:13.027Z
2010-11-08T13:28:13.027Z
Peter Shor 
<p>A paper of mine with Gupta and Kumar titled <a href="https://www.sciencedirect.com/science/article/pii/S0166218X05000934" rel="nofollow noreferrer">On a bidirected relaxation for the MULTIWAY CUT problem</a> was also based on running experiments. In fact we were trying to prove the converse of what we ended up proving. Vazirani, in the first edition of his book on approximation algorithms, suggested that the bidirected relaxation was at least as good as the relaxation used by Calinescu-Karloff-Rabani. In running experiments we saw that CKR relaxation was always as good as the bidirected relaxation! And we proved that this was indeed the case. Vazirani also stated that the bidirected relaxation was invariant to the order of the terminals. The paper falsified this. Running experiments showed that different orders were giving different values for the relaxation.</p>

CC BY-SA 4.0
2021-02-20T06:31:10.633Z
2021-02-20T06:31:10.633Z
Chandra Chekuri
<p>My recent paper with Karthik Chandrasekharan titled <a href="https://arxiv.org/pdf/2009.12442.pdf" rel="nofollow noreferrer">Hypergraph <span class="math-container">$k$</span>-cut in deterministic polynomial time</a> was based on extensive computational experiments. We explored different conjectures and submodular functions and found counter examples to several different approaches. The truth of the main structural theorem was suggested by experiments and we then proved it by hand. We acknowledge this in the paper.</p>

CC BY-SA 4.0
2021-02-20T06:24:48.040Z
2021-02-20T06:24:48.040Z
Chandra Chekuri
<p>Some recent results in <a href="https://cstheory.stackexchange.com/questions/14166/the-significance-of-state-complexity-in-automata-and-regular-languages">state complexity</a> were found with the help of systematic brute-force search for worst-case examples. This is doable because there are not too many deterministic finite automata with a small number of states, for example if we concentrate on binary or ternary alphabets. Also, in many cases there are families of worst-case examples for <span class="math-container">$1,2,3,4,5$</span> states and so on, and not only for all numbers of states <span class="math-container">$n$</span> that are greater than some large-ish <span class="math-container">$n_0$</span>.</p>
<p>I've found this explicitly described in the introduction of the following paper.</p>
<p><a href="https://doi.org/10.1016/j.ic.2008.03.018" rel="nofollow noreferrer">Guangwu Liu, Carlos Martin-Vide, Arto Salomaa, Sheng Yu: State complexity of basic language operations combined with reversal. Information and Computation 206 (2008) 1178–1186</a></p>
<p>The relevant quote is as follows:</p>
<blockquote>
<p>All the main results presented in this paper, especially the lower bound results, were obtained with the help of a large
number of experiments using computer software. For obtaining the tight lower bound for the reversal of union, for example,
we first proposed possible examples from our experiences. Then we checked the examples using our computer software
Grail+. There were many iterations in modifying the examples and checking by the software again. After satisfying examples
were obtained with experiments, we tried to prove the result theoretically. When we had problems in obtaining a theoretical
proof, we were back to experiments again. We consider that this is a relatively new approach in theoretical computer science
research. We think that our results presented in the paper would be very difficult to obtain without this new approach.</p>
</blockquote>
<p>For many results in state complexity, the upper bounds are from standard constructions, and the difficult part is to find worst-case examples and prove the tight lower bound. Many of the previous papers on state complexity discussed the proofs and did not lay out how the examples were found. But I remember that in 2008, the above method already had been around for at least a few years, and was considered a trick of the trade.</p>
<p>By the way, I think that also many results in state complexity are and were obtained without the computer assisted method, but in the traditional way of doing mathematics.</p>

CC BY-SA 4.0
2021-02-19T15:44:34.443Z
2021-02-19T15:44:34.443Z
Hermann Gruber
<p>In 2018, Aubrey de Grey <a href="https://arxiv.org/abs/1804.02385" rel="nofollow noreferrer">found</a> a 1581-vertex, non-4-colourable unit-distance graph. This gives a lower bound of five for the famous <a href="https://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem" rel="nofollow noreferrer">Hadwiger-Nelson problem</a>. He used a computer to verify that the graph indeed has chromatic number at least five. <a href="https://gilkalai.wordpress.com/2018/04/10/aubrey-de-grey-the-chromatic-number-of-the-plane-is-at-least-5/" rel="nofollow noreferrer">Gil Kalai's blogpost</a> covers some facts and further developments.</p>
<p>An <a href="https://www.quantamagazine.org/decades-old-graph-problem-yields-to-amateur-mathematician-20180417/" rel="nofollow noreferrer">article</a> in the quanta magazine reports that he also found the example graph &quot;with minimal computer assistance&quot;. That is, he used the computer twice for his result: first, he used it (a bit) to <em>find</em> the example, and then he used it (more heavily) to <em>verify</em> that his example really does the job.</p>

CC BY-SA 4.0
2021-02-19T11:39:10.837Z
2021-02-19T11:39:10.837Z
Hermann Gruber
<p>The purposes of this question is to collect examples from theoretical computer science where the systematic use of computers was helpful</p>

<ol>
<li>in building a conjecture that lead to a theorem,</li>
<li>falsifying a conjecture or proof approach,</li>
<li>constructing/verifying (parts of) a proof.</li>
</ol>

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

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

CC BY-SA 3.0
2012-09-20T17:21:10.407Z
fyi similar to mathoverflow, [Interesting conjectures “discovered” by computers and proved by humans?](http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans)
vzn
CC BY-SA 2.5
2010-08-18T16:03:31.627Z
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
CC BY-SA 2.5
2010-11-08T15:14:30.263Z
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
<proofs><survey><examples><proof-techniques>
Where and how did computers help prove a theorem?
Moritz
# Where and how did computers help prove a theorem?

(Asked by: username_0 on 2010-08-17)

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

**Tags:** proofs, survey, examples, proof-techniques
> **Comments:**
> **username_0**: 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.  
> **username_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!  
> **username_1**: fyi similar to mathoverflow, [Interesting conjectures “discovered” by computers and proved by humans?](http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans)  

---

## 18 answers

### Answer by username_3 on 2010-08-17. Score: 33

A very well-known example is the [Four Color Theorem](http://en.wikipedia.org/wiki/Four_color_theorem), originally proven by exhaustive checking.

> **Comments:**
> **username_4**: (Arguably) not theoretical computer science.  

---

### Answer by username_5 on 2010-08-17. Score: 23

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](http://www.math.rutgers.edu/~zeilberg/GT.html), and another program to prove a class of [combinatorial identities](http://www.math.temple.edu/~akalu/html/pg1.html). Some of the methods are mentioned in the book [A=B](http://www.math.upenn.edu/~wilf/AeqB.html).


---

### Answer by username_6 on 2010-08-19. Score: 22

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!

> **Comments:**
> **username_7**: Yeah, I like it too.  

---

### Answer by username_8 on 2010-08-17. Score: 20

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](http://arxiv.org/abs/cs/0601002), 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 by username_9 on 2010-08-17. Score: 20

Thomas Hales proof (his site, [MathSciNet](http://www.ams.org/mathscinet-getitem?mr=2179728)) 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](http://code.google.com/p/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 by username_10 on 2010-08-17. Score: 19

A counterexample to the [Hirsch conjecture](http://en.wikipedia.org/wiki/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](http://gilkalai.wordpress.com/2010/06/15/a-counterexample-to-the-hirsch-conjecture-is-now-out/#comments) or the [paper on arxiv](http://arxiv.org/abs/1006.2814).


---

### Answer by username_11 on 2010-11-08. Score: 17

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.

> **Comments:**
> **username_2**: 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.  

---

### Answer by username_12 on 2010-08-17. Score: 14

The [Karloff–Zwick algorithm](http://en.wikipedia.org/wiki/Karloff%E2%80%93Zwick_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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.3939).

Besides Hales' proof to the Kepler conjecture as mentioned above, the proof to the [Honeycomb conjecture](http://en.wikipedia.org/wiki/Honeycomb_conjecture) and the one to the [Dodecahedral conjecture](http://en.wikipedia.org/wiki/Dodecahedral_conjecture) are computer aided as well.

> **Comments:**
> **username_13**: While we're in this vein, Weaire and Phelan's disproof of the Kelvin conjecture was also computer-aided. (http://en.wikipedia.org/wiki/Weaire%E2%80%93Phelan_structure)  

---

### Answer by username_14 on 2010-08-18. Score: 13

You can check out Shalosh B. Ekhad's [homepage](http://www.math.rutgers.edu/~zeilberg/ekhad/papers.html). This computer has been publishing papers for a while (usually with coauthors).


---

### Answer by username_15 on 2010-08-23. Score: 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 by username_16 on 2010-08-18. Score: 10

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](http://rads.stackoverflow.com/amzn/click/0521585333) describing how it was done.


---

### Answer by username_4 on 2010-08-17. Score: 10

The results in "[The Geometry of Binary Search Trees](http://www.siam.org/proceedings/soda/2009/SODA09_055_demainee.pdf)" 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.)

> **Comments:**
> **username_18**: By "asses" I assume you mean "Arborally Satisfied Sets"? Maybe I have given away the fun of the acronym. :)  

---

### Answer by username_17 on 2010-08-23. Score: 8

The formula for the [Bailey-Borwein-Plouffe algorithm](http://en.wikipedia.org/wiki/Bailey%E2%80%93Borwein%E2%80%93Plouffe_formula) to compute the nth bit of Pi without computing any of the more significant bits was discovered, [according to Simon Plouffe](http://groups.google.com/group/sci.math.symbolic/msg/5b7e62ce42ae0cb6?pli=1), using computer proof systems.


---

### Answer by username_13 on 2010-11-08. Score: 7

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.


---

### Answer by username_19 on 2021-02-20. Score: 2

A paper of mine with Gupta and Kumar titled [On a bidirected relaxation for the MULTIWAY CUT problem](https://www.sciencedirect.com/science/article/pii/S0166218X05000934) was also based on running experiments. In fact we were trying to prove the converse of what we ended up proving. Vazirani, in the first edition of his book on approximation algorithms, suggested that the bidirected relaxation was at least as good as the relaxation used by Calinescu-Karloff-Rabani. In running experiments we saw that CKR relaxation was always as good as the bidirected relaxation! And we proved that this was indeed the case. Vazirani also stated that the bidirected relaxation was invariant to the order of the terminals. The paper falsified this. Running experiments showed that different orders were giving different values for the relaxation.


---

### Answer by username_19 on 2021-02-20. Score: 1

My recent paper with Karthik Chandrasekharan titled [Hypergraph $k$-cut in deterministic polynomial time](https://arxiv.org/pdf/2009.12442.pdf) was based on extensive computational experiments. We explored different conjectures and submodular functions and found counter examples to several different approaches. The truth of the main structural theorem was suggested by experiments and we then proved it by hand. We acknowledge this in the paper.


---

### Answer by username_20 on 2021-02-19. Score: 1

Some recent results in [state complexity](https://cstheory.stackexchange.com/questions/14166/the-significance-of-state-complexity-in-automata-and-regular-languages) were found with the help of systematic brute-force search for worst-case examples. This is doable because there are not too many deterministic finite automata with a small number of states, for example if we concentrate on binary or ternary alphabets. Also, in many cases there are families of worst-case examples for $1,2,3,4,5$ states and so on, and not only for all numbers of states $n$ that are greater than some large-ish $n\_0$.

I've found this explicitly described in the introduction of the following paper.

[Guangwu Liu, Carlos Martin-Vide, Arto Salomaa, Sheng Yu: State complexity of basic language operations combined with reversal. Information and Computation 206 (2008) 1178–1186](https://doi.org/10.1016/j.ic.2008.03.018)

The relevant quote is as follows:

> All the main results presented in this paper, especially the lower bound results, were obtained with the help of a large
> number of experiments using computer software. For obtaining the tight lower bound for the reversal of union, for example,
> we first proposed possible examples from our experiences. Then we checked the examples using our computer software
> Grail+. There were many iterations in modifying the examples and checking by the software again. After satisfying examples
> were obtained with experiments, we tried to prove the result theoretically. When we had problems in obtaining a theoretical
> proof, we were back to experiments again. We consider that this is a relatively new approach in theoretical computer science
> research. We think that our results presented in the paper would be very difficult to obtain without this new approach.

For many results in state complexity, the upper bounds are from standard constructions, and the difficult part is to find worst-case examples and prove the tight lower bound. Many of the previous papers on state complexity discussed the proofs and did not lay out how the examples were found. But I remember that in 2008, the above method already had been around for at least a few years, and was considered a trick of the trade.

By the way, I think that also many results in state complexity are and were obtained without the computer assisted method, but in the traditional way of doing mathematics.


---

### Answer by username_20 on 2021-02-19. Score: 1

In 2018, Aubrey de Grey [found](https://arxiv.org/abs/1804.02385) a 1581-vertex, non-4-colourable unit-distance graph. This gives a lower bound of five for the famous [Hadwiger-Nelson problem](https://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem). He used a computer to verify that the graph indeed has chromatic number at least five. [Gil Kalai's blogpost](https://gilkalai.wordpress.com/2018/04/10/aubrey-de-grey-the-chromatic-number-of-the-plane-is-at-least-5/) covers some facts and further developments.

An [article](https://www.quantamagazine.org/decades-old-graph-problem-yields-to-amateur-mathematician-20180417/) in the quanta magazine reports that he also found the example graph "with minimal computer assistance". That is, he used the computer twice for his result: first, he used it (a bit) to *find* the example, and then he used it (more heavily) to *verify* that his example really does the job.


---

