11 ms·

> Possible: tools such as Lean will begin to do research semi-autonomously, perhaps uncover problems in the literature. Maybe these tools will replace research

> Possible: tools such as Lean will begin to do research semi-autonomously, perhaps uncover problems in the literature. Maybe these tools will replace research mathematicians. > In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years. I wonder whether automated mathematics software would really be able to compete with humans at explaining how areas of mathematics fit together and what roles different mathematical objects play. I'm not a mathematician so sorry for the simplistic example, but for example, would automated mathematics software be able to do something like (a) invent the complex numbers (i.e. as an object in algebra -- a "field extension" of the reals), and (b) also make a statement like "these are useful for modeling cyclical/oscillatory behavior"?

Someone 7y ago
One could cluster theorems and types by “connectedness”, but even then, I don’t think “algebra” would stand out as separate from, say, “geometry” or “number theory”. Those are just stickers ignorant humans put on things they thought to be significant entities centuries ago. Chances are not even “arithmetic” would stand out as a separate entity. Even if it did, the computer couldn’t give it a name that makes sense to humans. And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever.
- Myrmornis 7y ago
  > And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever. I don’t think that’s really true. There are cyclical/oscillatory behaviors within pure mathematics, for which complex numbers are useful. Just look at the other math article that’s on HN front page currently, on the Riemann Zeta function (John Baez blog post).
whatshisface 7y ago
I think the image is the computer acting as the world's most brilliant grad student, solving lemmas instantly while the mathematician makes value judgements while driving.
AlexCoventry 7y ago
> computers will be beating humans at math within ten years. I don't think anyone knows how long that's going to take. It's clear at this point that it's going to take something more than Deep Learning has to offer.
a_imho 7y ago
In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years. From my experience the track record of Outlandish Claims Made by People Having Vested Interest in Casting Them is rather poor. In fact, I can not recall a single one that was accurate.
- williamstein 7y ago
  I was at Buzzard's talk at Microsoft last week. Kevin spent a lot of time in the live talk explaining what he thinks Szegedy actually meant (there should eventually be video on youtube of this). Kevin clarified that in his opinion what Szegedy means by "math" isn't at all what Kevin means by "math", since it takes so long to get to the frontiers of research math. In particular, Kevin speculated that for Szegedy "math" is some specific research questions in combinatorics, which isn't at all what Kevin's view of "math" is. So Kevin's conclusion was that Szegedy really means that computers will beat humans at "something specific involving combinatorics" in the next ten years. Kevin wasn't optimistic about the same claim was about number theory, unless 10 years is replaced by "some day". Kevin also explained live in his talk that his main motivation for his recent interest in interactive theorem provers is a very bad experience he had a few years ago refereeing an important research paper by some famous mathematicians. That experience very much shook his faith in the ability of humans to do correct deep mathematics... I suppose from that perspective "computers will be beating humans" might just mean that humans are convinced of a (false!) result, but computers can't be convinced of that same false result (in the sense that nobody can formalize it). (Incidentally, some of the people at Kevin's talk were at Richard Stallman's talk in the same place the day before. Evidently RMS didn't allow any pictures or video, so not much will appear from that.)

Someone 7y ago

One could cluster theorems and types by “connectedness”, but even then, I don’t think “algebra” would stand out as separate from, say, “geometry” or “number theory”. Those are just stickers ignorant humans put on things they thought to be significant entities centuries ago. Chances are not even “arithmetic” would stand out as a separate entity. Even if it did, the computer couldn’t give it a name that makes sense to humans. And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever.

Myrmornis 7y ago
> And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever. I don’t think that’s really true. There are cyclical/oscillatory behaviors within pure mathematics, for which complex numbers are useful. Just look at the other math article that’s on HN front page currently, on the Riemann Zeta function (John Baez blog post).

whatshisface 7y ago

I think the image is the computer acting as the world's most brilliant grad student, solving lemmas instantly while the mathematician makes value judgements while driving.

AlexCoventry 7y ago

> computers will be beating humans at math within ten years. I don't think anyone knows how long that's going to take. It's clear at this point that it's going to take something more than Deep Learning has to offer.

a_imho 7y ago

In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years. From my experience the track record of Outlandish Claims Made by People Having Vested Interest in Casting Them is rather poor. In fact, I can not recall a single one that was accurate.

williamstein 7y ago
I was at Buzzard's talk at Microsoft last week. Kevin spent a lot of time in the live talk explaining what he thinks Szegedy actually meant (there should eventually be video on youtube of this). Kevin clarified that in his opinion what Szegedy means by "math" isn't at all what Kevin means by "math", since it takes so long to get to the frontiers of research math. In particular, Kevin speculated that for Szegedy "math" is some specific research questions in combinatorics, which isn't at all what Kevin's view of "math" is. So Kevin's conclusion was that Szegedy really means that computers will beat humans at "something specific involving combinatorics" in the next ten years. Kevin wasn't optimistic about the same claim was about number theory, unless 10 years is replaced by "some day". Kevin also explained live in his talk that his main motivation for his recent interest in interactive theorem provers is a very bad experience he had a few years ago refereeing an important research paper by some famous mathematicians. That experience very much shook his faith in the ability of humans to do correct deep mathematics... I suppose from that perspective "computers will be beating humans" might just mean that humans are convinced of a (false!) result, but computers can't be convinced of that same false result (in the sense that nobody can formalize it). (Incidentally, some of the people at Kevin's talk were at Richard Stallman's talk in the same place the day before. Evidently RMS didn't allow any pictures or video, so not much will appear from that.)