alt Hacker NewsOn the one-hand side, it's really impressive how LLMs drive mathematics forward, and this pace is only accelerating very quickly.
At the same time, most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter). LLMs do not care about "elegance" the way human beings do, which is a big advantage. LLMs for mathematics is such a great fit on many levels. Can't wait for a significant breakthrough, prove P=NP and all hell breaks loose.
Replies
> LLMs do not care about "elegance" the way human beings do, which is a big advantage.
It's just a matter of time before you can post train it for elegance too. Mathematical proofs in particular can be formally verified automatically which is a big advantage.
> most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter)
How do you know they're correct if they're super messy and chaotic?
I agree, counterexample to P!=NP would be great. I tried but it's a mess.
Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
Sure they care about elegance, or at least brevity. Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems. It doesn't mean they are perfect at it though.
The mathematics is to a great extent about understanding of abstract structures. As humans, we prefer simple structures/proofs (I suspect that is to a great extent because those are easier to understand), and as such find elegance in simplicity.
In fact, the capability of the human brain to understand complex structures and proofs is rather limited.
LLMs (hmm, I would prefer to use 'AI solver', as LLM is nowadays just a part of it) finding a complex proof can mean several things: 1) AI by its nature/construction does not have preference for simple stuff (it 'thinks' differently than human: a human will, in its search for a proof, start by exploring the 'simpler' parts of the proof space, and hence more likely find a 'simple' proof, while a AI might be more target oriented and descend deeply in depth-first-search manner to recursively solve sub-tasks, without much regard about the overall simplicity of the proof). This can be eventually solved, by subsequent 'polishing' passes, similarly as things work in human science.
2) there might simply not exist a simple/elegant proof of a given problem. The world is a complex beast. Its just our brains trying to find simple/elegant meaning/structure, even in places where there is none.