From Wired: "As Math Grows More Complex, Will Computers Reign?"

From an interesting article in Wired from earlier this month:

Computers are now used extensively to discover new conjectures by finding patterns in data or equations, but they cannot conceptualize them within a larger theory, the way humans do. Computers also tend to bypass the theory-building process when proving theorems, said Constantin Teleman, a professor at the University of California at Berkeley who does not use computers in his work. In his opinion, that’s the problem. “Pure mathematics is not just about knowing the answer; it’s about understanding,” Teleman said. “If all you have come up with is ‘the computer checked a million cases,’ then that’s a failure of understanding.”

Zeilberger disagrees. If humans can understand a proof, he says, it must be a trivial one. In the never-ending pursuit of mathematical progress, Zeilberger thinks humanity is losing its edge. Intuitive leaps and an ability to think abstractly gave us an early lead, he argues, but ultimately, the unswerving logic of 1′s and 0′s — guided by human programmers — will far outstrip our conceptual understanding, just as it did in chess. (Computers now consistently beat grandmasters.)

“Most of the things done by humans will be done easily by computers in 20 or 30 years,” Zeilberger said. “It’s already true in some parts of mathematics; a lot of papers published today done by humans are already obsolete and can be done using algorithms. Some of the problems we do today are completely uninteresting but are done because it’s something that humans can do.”

Since the set of possible mathematical proofs is infinite, computers will never "discover" all mathematical proofs. They might discover all proofs within a finite set of parameters -- and so they might exhaust a "branch" of mathematics if it is sufficiently well defined (or at least elucidate all possible non-trivial/non-redundant proofs in a well defined branch).

The strength of computers, though, lies not just in validating proofs -- and for this computer validation can sometimes be the gold standard -- but in the possibility of mapping relations. Mapping relations allows trends and unexpected connections to be uncovered; those are the foundation of theoretical mathematical developments. Once sensed a theory can be cobbled together to explain them; such a theory is suggested by the relationship or by hit and miss analysis of postulates for the relationship. there is no reason computers cannot eventually be programmed to do this better than people -- there's no theoretical bar to it.

In other words, short of some seismic change in trends, computers will eventually exceed all humans in theoretical mathematical ability. I don't think that can be legitimately disputed.

I'm just saying.