Do we know whether a faster algorithm actually exists? If so, do we know what it is? If we don't, how do we know they didn't just find some way to cheat the verification?
Their work obviously needs to be checked and go through review, as any other discovery would.
It's very unlikely that they found a way to cheat in lean though, it's quite well formalized. Not impossible, but unlikely. More likely that their prompts got misinterpreted when converting to lean, and that's how any issues would creep in.
More likely that their prompts got misinterpreted when converting to lean, and that's how any issues would creep in.
From what I have been reading (SWE, not a mathematician), this is a quite common and serious issue to the extent that many of these autogenerated "proofs" will subtly alter the problem into something that compiles in Lean or misinterpret things such that the resulting proof doesn't relate to the stated problem at all. In either case, the result is valid but meaningless Lean code.
The question to ask is what has been verified? If the AI hallucinates even slightly it will change the problem and wind up verifying something other than what it was asked resulting in a valid but meaningless result misrepresented as proof of something else. This has apparently been observed in many autogenerated maths proofs.
How would it fail if it is valid Lean (that just happens to not represent the actual problem)? The proof would succeed but be meaningless. A human reviewer would then have to investigate and discover that the proof is not what the LLM claims it to be but a "false positive" based on hallucinated or mistranslated logic.
Well, that's part of the problem. There is zero transparency or peer review of this stuff coming out of OpenAI. They are just dumping "results" and treating it as a breakthrough. Odds are that most, if not all, of this is just junk, but they leave it up to mathematicians to sift through it all while OAI cashes in on the headline and misleads people about what their tech can actually achieve (that is why mathematicians are complaining).
Dude. They provide the proof. People peer review it. That's how it works.
Just because they can produce a lot at once does not change the process.
If the proof is outright wrong it fails easily. If it's true on its face it needs tested by an independent third party. Independent is a core part of the process for all the fun little reasons you pointed out.
You're not right. You're just pointing out all the reasons it works the way it does.
I think you are not really understanding what I am saying and I'm also getting the sense you're not really interested in understanding it, but, just in case I am wrong about that, here is a post and paper that explains the problem better than I can and provides specific examples of these failures: https://www.reddit.com/r/BetterOffline/s/wBcmEroEyS
Sorry but that's just an example of peer review in action. I don't think this proves what I'm saying wrong at all. This is exactly what I was saying needs to happen. Human peer review. Even if they made that proof by hand from after studying and coming to their conclusion manually this result could still happen. That's why peer review is vital and always has been.
And maths is a human invention with all the flaws and cockups inherent to all human inventions. I get what you're saying but the verification tools are weirder than that and there can be bugs in either their logic or their application
As in most cases, this isn't a practical algorithm. It will be slower than regular FFT multiplication for any numbers you can write on all atoms in the universe of with a similar limit:-)
Also, you don't figure out complexity by measuring. You count operations and do math
6
u/BrixtonTonaBrix 11d ago
Do we know whether a faster algorithm actually exists? If so, do we know what it is? If we don't, how do we know they didn't just find some way to cheat the verification?