Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)
replyMaybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.
replyI don't think it will be a problem for long, as AI systems evolve they will be able to find those elegant solutions and explanations for you in due time...
replyAI does not care for elegance. That's one of the problems with the bulk of AI generated code: even if it does the job it is between 3 and 5x as much code as you would normally use to do the same thing. And even if we conclude that this is fine as long as the tests pass it is a massive barrier to understanding. Good code is easy to read. AI generated code - the bulk of the AI generated code that I've been exposed to to date, to be more precise - is overly complicated. Elegance is to do that which needs doing, no more, no less.
replyI doubt that. I don't think AI are trained to find elegant solutions, they are trained to find solutions. if you look at the things that OpenAI published, so seem to be micro improvements riddled with chaos. They are better solution, but they aren't drastic.
replyI have noticed this with autoresearch too, the solutions and improvments that you get are incremental and not groundbreaking. Humans, have a way find elegant solutions and also seem to solve that problem. Then again, beauty is in the eye of the beholder, and I might be wrong.
Yes, spot on. I think it has to do with the lack of emotion. Humans enjoy finding something beautiful.
reply> "The problem of the proof was that we knew that FCT was true"
replyCitation needed.
That was terrible phrasing. I meant "The problem with the proof was that although it showed that FCT was true, the proof did not explain why".
replyYeah. On a similar note, without the computer aspect, I once had a prof tell me that he did not like character theory. If I remember right, there you calculate some numbers from a group and can prove some properties about it. But you gain no understanding of why those properties hold.
reply> the proof did not explain why
replySo humans do/did still have a role to play
[dead]
reply