> 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?
Do you have any argument why you might think this would be true?
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.
Of course it also contains more than enough information to learn what kind of question is interesting to humans.