logoalt Hacker News

muldvarpyesterday at 3:41 PM1 replyview on HN

> 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?


Replies

pfdietzyesterday at 3:59 PM

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.

show 1 reply