Mathematical concepts motivated by computational results

Question

What are some interesting and important pure mathematics concepts, results or theorems that have been motivated, discovered, or proven using computers/computational methods?

I know little about these things, but I wonder whether there are perhaps some interesting results in say algebra, that were proven using automated proving systems. In number theory there's probably results that were motivated by an observation that was checked up to a large number, but I don't know of anything concrete. Lastly, the Mandelbrot set seems to be a good example of a concept that was found to be interesting after a visualization using computers.

Answer 1

The Erdos discrepancy problem was proved for the $c=2$ case by a method of SAT solving and a bit later fully proved by Terrence Tao.

Answer 2

The https://en.wikipedia.org/wiki/Birch_and_Swinnerton-Dyer_conjecture, one of the Millenium Prize Problems was motivated by results of computer calculationns (done in the 1960s !). See the history section of the Wikipedia text.

Answer 3

Computability was established as a mathematical concept before the electronic computer was invented, but the whole field of computational complexity probably wouldn't exist without computers to motivate it. Though it's usually classified as a branch of theoretical computer science, it is mathematics enough that the P vs NP problem is included among the Millennium Prize Problems.

In the same general direction, many basic results in formal language theory owe their formulation to their utility in constructing compilers for programming languages.

Answer 4

The four-color theorem is a famous example of an interesting theorem whose only known proofs all rely on computer verification rather than on human readers signing off on all the details.

Answer 5

A theorem prover was the first to establish that Robbins algebras are Boolean. Extensive computer work as well as a proof assistant were used to prove the Kepler conjecture. Stringology was motivated by computers.