Comment by fhdkweig
6 days ago
The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.
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)
> the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find
Kempe's reduction technique, on which the eventual proof still depended (at least spiritually? I think?), did contain true insight with reach beyond the original problem statement (e.g., Chaitin/register allocation).
I submit that "clever way to soundly reduce to finite set and check" is itself probably one of the more important types of insight in mathematics. Actually, all of my favorite mathematics, from an aesthetic perspective, has exactly this flavor. That's down to taste, of course, but it is sort of a fundamental/powerful move in modern mathematics. The beauty of that insight can only be appreciated once you're willing to accept that boring case checking is tractable.
In that sense, the FCT gave us two really important insights -- first some profound insight from Kempe then an equally profound insight about the role of computers as a bicycle for human thought.
Yeah, not saying the proof was worthless, and the technique is indeed a genuine insight. However, there's likely to be a proof that explains why all the cases work out rather than it just being a crazy coincidence, and the existence of the proof did stifle further research into the now "solved" problem.
In hindsight, along with illustrating the potential of computers as a bicycle for the mind it also gave the first indication that if such proofs were to become very easy to produce they could also be used as a bulldozer to bury the mind.
Maybe 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.
I 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...
AI 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.
AI cares for whatever you reward it for, but we don't seem to care about elegance much either.
I 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.
I 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.
Until elegance can be trained through RLVF, it will not be elegant. A lot of problems in AI seem to be finding ways to bring RLVF to more domains, as the current "spikiness" of AI seems to be mostly related to how effective RL is for a particular domain (if you need RLHF you are fucked and it's why it has not gotten better at writing and individual models still have "styles")
Yes, spot on. I think it has to do with the lack of emotion. Humans enjoy finding something beautiful.
Maybe the open problems are just by nature non-elegant and we human beings are bad at non-elegant mathmatics and found them either hard or not interesting before.
It does though. To reduce from infinitely many graphs to a finite number of cases there is a lot of insight by itself.
Exactly.
> "The problem of the proof was that we knew that FCT was true"
Citation 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".
Yeah. 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.
> the proof did not explain why
So humans do/did still have a role to play
5 replies →
[dead]