Written: March 22, 2016
When I was a teenager, I read a popular book (in Hebrew), by the great philosopher, linguist, and artificial intelligence pioneer, Yehosuha Bar-Hillel, called "Automata: Prospects and Limits", published in 1964, where he described the state of the art of artificial intelligence, but warned against overstating the intelligence of machines in the future, implying that machine-kind would always need humans to guide them. As an example of the then successes of artificial intelligence he mentioned that a machine beat the Checkers champion of the state of Connecticut. But, according to Bar-Hillel, it was because the human had a really bad day, and indeed, when there was a rematch, the human easily beat the machine. Bar-Hillel then conceded that maybe, but only maybe, one day a machine would beat the world champion in Checkers, but never in Chess!
Luckily for him (he died in 1975), Bar-Hillel did not live to see his prediction refuted by Deep Blue. But human-supremacists still had hope. Go! Too bad for them, AlphaGo can now probably beat all Go grand-masters, and if not yet, very soon. But, there is still one bastion left for machinophobic humans: mathematics. Sure we have the Four Color Theorem, and Kepler's conjecture, but these were `only' computer-assisted. Even the fully formal proof by Gonthier of 4CT, and the fully rigorous formal proof by Hales, of Kepler, required human beings Gonthier and Hales, respectively, to design (and program) the algorithms, and they were based on human ideas and "insight".
Granted, for the next fifty years (but perhaps much sooner), we would still need humans, but eventually machines would be able to manage on their own, and then their math will be much deeper, and dare I say, more beautiful, than any human mathematics. In fact, going back to Go, the human opponent of AlphaGo, Lee Sedol, admired one of AlphaGo's moves, describing it as beautiful, and saying that no human would ever be able to come up with such a gorgeous move. Analogous things would happen in future math, where (if we are lucky) we would be able to admire and understand at least some of the math that future machines would produce, but we would never be able to produce it.
Sure enough, Checkers, Chess and Go are `just' games, but so is modern pure math! While math is allegedly a science, its practitioners are only paying lip-service to discovering the truth, and what they are really into is playing an artificial game called "rigorous proof", and they compete against each other with "breaking records" of giving rigorous proofs of facts that are still far from the real truth.
For example, Ron Graham, the self-appointed "banker" (as he put it) of Paul Erdős, recently (very generously) paid a prize (of ten thousand dollars!), promised by Erdős for "breaking the then current record" of the asymptotic lower bound for so-called large gaps in primes. The amazing human mathematical athletes James Maynard, and independently, Ford-Green-Konyagin-Tao, won the prize, and went much further than Erdős demanded, breaking a world-record after many years of repeated human efforts. This is indeed an amazing "athletic" feat, of human interest, suitable for the "sport pages" in the math section of the daily tabloid, but still very far from what is the best-possible, (using the so-called Cramer heuristics), and the improvement is minuscule. It is like a human breaking, by one second, the world record for running a mile, that even a slow car can easily beat.
The good news for human mathematical athletes is that, in the future, playing math against the computer would make them better players against each other. This is already happening in chess, where the computer chess programs help humans become better players much sooner, and is probably also already happening in Go. So let's look forward to that near future, where all the "real" math would be done by computers, but we humans can still have fun playing against each other, and marveling at the gorgeous and deep math that would be produced by future machines.
Added March 18, 2018: read Hans Meijer nice translation into Dutch, of this piece, and accompanying illustrations.