This week the New Yorker has a profile of Magnus Carlsen, a young Norwegian chess player that is currently the #2 ranked player in the world (he has been #1 in the past).

The article discusses how the game has been changed by the availability of computer programs that are now unbeatable even by the top players, and the fact that the younger generation of players (but not Carlsen) grew up playing against computer programs. The following quote was interesting:

Computers have no skills and they have nothing approaching intuition. Carlsen finds their games inelegant, and complains about “weird computer moves I can’t understand,” whereas in talking about his own game he speaks of achieving “harmony” among the pieces on the chessboard, and even of “poetry.”

It struck me that we could see in our lifetime computer programs becoming better than human mathematicians in raw technical skills, and that the above quote could reflect our future attitude toward proofs found by computers. “Where is the statement of this lemma coming from?”, “this argument has no elegance!”, and so on.

### Like this:

Like Loading...

*Related*

“Where is the statement of this lemma coming from?” – No need to wait for the future. It can be said about even currently written papers.

“this argument has no elegance!”, Yes,that is the case,I don’t like forceful proof by computer without elegance.

I mean brute proof by “forceful proof”,I’d think almost proof by computer are rude .

Thanks and Praises to The Mighty Computer and to Z

Some concerns are justified. Others are simply the words of technophobes, e.g. some mathematicians that still dismiss the four color theorem proof.

However, computer proofs would have to come from a deterministic system that guarantees the statement is true, while chess programs don’t have the time to select the optimal move, so heuristics are used.

There is a quantity/quality dynamic at play here. A proof where we consider 2 or 3 cases, resolve them, and present our result is rather nice on the face of it. If there are 12 or 40 cases then it becomes rather difficult to hold it all in your head. If there are 19 billion cases we call it brute force.

Often, elegance is associated with brevity. Brevity is compression. Compression means finding patterns. Finding patterns means finding models. Good models are elegant models. Repeat.

A computer-generated proof wouldn’t have to be a long case analysis as in the 4-color theorem. Already with current “technology” we see computer-assisted proofs in which the computer proves inequalities or identities via long and mystifying symbolic manipulations, or by finding feasible solutions to the duals of certain linear programs.

But if natural language processing and basic theorem-proving algorithms improve, we could get programs that given a typical math paper would be able to get the correct formal meaning of most statements and be able to reconstruct a valid proof for a small fraction of them. Use such a program on all the papers in the arxiv, and you can reconstruct a very large set of verified statements, and also extract statistical rules of what kind of approach works to prove what kind of statement.

Given a statement that one is interested in proving, such a system might discover an essentially equivalent version in a paper in an entirely unrelated area, and adjust the proof as required but it might also pull together a dozen results them unrelated areas, and combine them with a series of very long and incomprehensible derivations.

I guess I keep going back to Bill Thurston’s comment (paraphrased) that the only point of a proof is to help understand. In that sense, an incomprehensible but correct proof is akin to a zero knowledge proof.

Pingback: Weekly picks « Mathblogging.org — the Blog

A human-done proof that seems about as bad as I could imagine computer-generated ones being is the one done for Fermat’s Last Theorem.

Contrary to Fermat’s imagination that he had a proof that was a little too large to fit in the margin, Wiles’ general proof involved fields that didn’t exist until the 20th century, and is incomprehensible to all but a relative handful of mathematicians.

Computer generated proofs, thus far, have a habit of being insufficiently parsimonious to be readily understood, which amounts to much the same as with Wiles’ proof of FLT.

Whether we’re talking about:

a) Patterns in chess,

b) Structures of proofs,

c) Structures of Rubik’s Cube solutions,

d) Factorizations of polynomials (or other such expansions that might be done by equation solvers like Macsyma, Maple, and such)

they all have pretty material commonalities.

Doing a computerized combinatorial expansion may allow arriving at a solution, but it’s entirely possible that this solution won’t provide anyone with an ability to reason about that solution, or to reuse aspects of the solution’s structure to help understand some other problem.

Yep, that it’s “not elegant” does matter somewhat.

Pingback: The Prince’s Gambit « For Madmen Only

A different prediction, closer to what I believe, is that computers will not become truly good at doing mathematics unless they learn to find beautiful, elegant, explanatory proofs. The rough reason: searching for beautiful explanatory proofs is much less like an NP-complete problem than searching for arbitrary and incomprehensible proofs.

Pingback: Second Xamuel.com Linkfest