Groups and coloring
The classification of finite simple groups is one of the crowning achievements of pure mathematics. A group is a mathematical object that measures symmetry. Simple groups are special in that they have no non-trivial normal subgroups. You can think of simple groups as the basic elements from which all other groups can be formed. Taking up over ten thousand pages in dozens of papers, the proof of the classification is a testament to the power of human ingenuity.

The four color theorem is one of the best-known results in graph theory, stating that every map can be colored with four colors so neighboring countries get different colors. While this may seem easy for relatively small maps, the result applies to every possible map, or as we call them, planar graphs. All the known proofs of the four color theorem use a computer to check cases. While logical arguments reduce the number of cases significantly, computer assistance is essential to our present understanding of the proof.

These examples are opposites on the spectrum of the kinds of theorems mathematicians prove. For the classification of finite simple groups, mathematicians relied only on intuition and creativity. The proof of the classification was daunting, but with time and study, humans mastered it. For the four color theorem, while still relying considerably on our ingenuity, humans can’t presently duplicate the proof of the four color theorem without computer aid.
Modern computers meet mathematics
Computers are powerful tools in the tool chest of mathematicians. They allow us to probe deeper into mathematical truth, shining a light in the darkness. Two key applications of computers in mathematics these days are in case checking and simulations.
As in the four color theorem, if you have a conjecture that can be verified in a large but finite list of cases, then computers can make a big difference. Depending on the kind of problem you are studying, you can check thousands, millions, or even billions of cases. One of my graduate students Liam Baird did just that looking to find a 3-cop-win graph of order 10. There were thousands of cases to check, but he found a unique 3-cop-win graph of order 10: the Petersen graph. Later, we found a logical proof of this fact not using computers.

A second important application of computers in mathematics are simulations, where you run a model over time-steps. Mathematical models predict hurricanes, simulate neural networks, or mimic how social networks evolve over time. I encountered this approach when studying a certain model for complex networks. We guessed the model had a certain property, but it wasn’t until we ran simulations with hundreds of thousands of nodes that were we able to see it and eventually prove it.
There are countless examples like these, where computation gives mathematicians insights into realms of mathematics that otherwise would be impenetrable. There’s even a journal devoted in part to the use of computer-aided discovery in developing new mathematics. It’s called Experimental Mathematics.
Limits of computation
One key observation that is often overlooked by laypeople is that computers can only do finite mathematics. That is, they can only check a finite number of cases or run for a finite amount of time. A theorem with a universal quantifier over an infinite set can pose problems for computation. If you have a theorem about every map, or every simple group, or every prime number, then likely you will need to rely on a logical proof.
That is not to say that computers cannot prove theorems. They can and they do. Automated theorem proving uses logical systems to prove mathematical results. Most mathematicians think that the really “good stuff”, however, must rely on insights that humans, not machines, can make. I agree with that view—for example, I think a human will prove the Riemann hypothesis before any machine.
Gödel’s famous incompleteness theorem states that in any axiomatic system there are undecidable propositions. That is to say, in any formal system, such as one used by a computer, there will be properties unprovable by the system. Of course, these limits apply to what humans can prove also!

Creativity, Intuition, Insight
These are traits that humans have that machines don’t. Imagine a human and a computer waiting at a don’t walk sign on a very long road. The human notices that there are no cars around for miles and walks across the road. The machine is programmed to only cross the road when the light is green and so inefficiently waits for minutes before crossing. This simple analogy highlights our ability to improvise based on our environment. We use our senses and our gut instincts to do things that formal systems can’t.
Having said that, humans are illogical and our thinking is often erroneous. Plain and simple, we make mistakes. Far from being only negative qualities, however, those traits lead us down paths of discovery. By failing, we learn. It’s cliche but true.
Artificial intelligence (AI) can be viewed as the science of making and learning from mistakes. AI algorithms run many experiments, trying and failing until they get something right and “learn”. As computers are so much faster than humans, AI can run an enormous number of experiments until they find the correct solution. For example, AI can now beat any human at the complex board game of Go.

If there comes a time when computers begin proving various non-trivial mathematical results, then it is likely we will need to redefine mathematics. Mathematics will become whatever machines can’t do.
Prove me wrong!
Anthony Bonato