[nicf]

Well, it depends on exactly what future you were imagining. In a world where the model just spits out a totally impenetrable but formally verifiable Lean proof, then yes, absolutely, there's a lot for human mathematicians to do. But I don't see any particular reason things would have to stop there: why couldn't some model also spit out nice, beautiful explanations of why the result is true? We're certainly not there yet, but if we do get there, human mathematicians might not really be producing much of anything. What reason would there be to keep employing them all?

Like I said, I don't have any idea what's going to happen. The thing that makes me sad about these conversations is that the people I talk to sometimes don't seem to have any appreciation for the thing they say they want to dismantle. It might even be better for humanity on the whole to arrive in this future; I'm not arguing that one way or the other! Just that I think there's a chance it would involve losing something I really love, and that makes me sad.

[jebarker]

> The thing that makes me sad about these conversations is that the people I talk to sometimes don't seem to have any appreciation for the thing they say they want to dismantle

Yes! This is what frustrates my about the pursuit of AI for the arts too.

[zmgsabst]

This seems obviously untrue: why would they be replicating it if they didn’t want it?

I see both cases as people who aren’t well served by the artisanal version attempting to acquire a better-than-commoditized version because they want more of that thing to exist. We regularly have both things in furniture and don’t have any great moral crisis that chairs are produced mechanistically by machines. To me, both things sound like “how dare you buy IKEA furniture — you have no appreciation of woodwork!”

Maybe artisanal math proofs are more beautiful or some other aesthetic concern — but what I’d like is proofs that business models are stable and not full of holes constructed each time a new ML pipeline deploys; which is the sort of boring, rote work that most mathematicians are “too good” to work on. But they’re what’s needed to prevent, eg, the Amazon 2018 hiring freeze.

That’s the need that, eg, automated theorem proving truly solves — and mathematicians are being ignored (much like artist) by people they turn up their noses at.

[GPerson]

I don’t think the advent of superintelligence will lead to increased leisure time and increased well-being / easier lives. However, if it did I wouldn’t mind redundantly learning the mathematics with the help of the AI. It’s intrinsically interesting and ultimately I don’t care to impress anybody, except to the extent it’s necessary to be employable.

[nicf]

I would love that too. In fact, I already spend a good amount of my free time redundantly learning the mathematics that was produced by humans, and I have fun doing it. The thing that makes me sad to imagine --- and again, this is not a prediction --- is the loss of the community of human mathematicians that we have right now.

[nonethewiser]

>But I don't see any particular reason things would have to stop there: why couldn't some model also spit out nice, beautiful explanations of why the result is true?

Oh… I didnt anticipate this would bother you. Would it be fair to say that its not that you like understanding why its true, because you have that here, but that you like process of discovering why?

Perhaps thats what you meant originally. But my understanding was that you were primarily just concerned with understanding why, not being the one to discover why.

[nicf]

This is an interesting question! You're giving me a chance to reflect a little more than I did when I wrote that last comment.

I can only speak for myself, but it's not that I care a lot about me personally being the first one to discover some new piece of mathematics. (If I did, I'd probably still be doing research, which I'm not.) There is something very satisfying about solving a problem for yourself rather than being handed the answer, though, even if it's not an original problem. It's the same reason some people like doing sudokus, and why those people wouldn't respond well to being told that they could save a lot of time if they just used a sudoku solver or looked up the answer in the back of the book.

But that's not really what I'm getting at in the sentence you're quoting --- people are still free to solve sudokus even though sudoku solvers exist, and the same would presumably be true of proving theorems in the world we're considering. The thing I'd be most worried about is the destruction of the community of mathematicians. If math were just a fun but useless hobby, like, I don't know, whittling or something, I think there would be way fewer people doing it. And there would be even fewer people doing it as deeply and intensely as they are now when it's their full-time job. And as someone who likes math a lot, I don't love the idea of that happening.