[pfdietz]

Proving theorems will have lower payoff, but posing new questions (for AI to chew on) will have higher payoff. Math will go from theorem proving to conjecture farming/exploration. In a way this could be even more fun.

Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems.

[tacomonstrous]

Yes, as someone who prefers developing the 'correct' structure over 'merely' proving theorems, this is good for me in the short term. However, the writing I fear is on the wall for my medium and long term utility.

[muldvarp]

> Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems.

Do you have any argument why you might think this would be true?

[pfdietz]

For theorem proving, once the statement is formalized, there's an oracle for correctness of the proof. For deciding if something is interesting, well, de gustibus non est disputandum, you know?

Experience with Lenat's AM decades ago had it go off making all sorts of uninteresting hypotheses. That's very weak evidence, of course.

This suggests people also have role for fundung "beautiful" or "the best" proofs, since that also involves taste. More generally, perhaps the role of people is to reveal their preferences, and that requires people be in the loop somehow. Maybe "math criticism" becomes the job. And if AI is to serve people in general, it needs to know these preferences.

[muldvarp]

I think the training data contains more than enough information for an LLM to learn what kind of proof is considered beautiful or elegant by humans.

Of course it also contains more than enough information to learn what kind of question is interesting to humans.