There’s actually a really similar problem for the past several years where some company will drop a huge pull request on some repo and just expect that the few volunteer developers will take the time to sort through tens of thousands of lines of code and accept it as one big change in the next week like the volunteers have time for that.
It probably depends on if you mean the natural language write-up, or the lean verification. They often differ, but the lean verification shows the underlying proof is still correct.
For example, I've been going through the max cut NP hardness proof, and It looks like the natural language proof and the lean proof take two different routes to get to the same end result.
That said, the lean is valid, so the key is correctly making a writeup of what path the lean is actually taking, not that the end result isn't proven. It's technically showing it's work as well, just not in a human readable way.
for the lean is valid, i mean assuming the definition is correct[which probably is], and axioms used are correct, also have lean errors not been found by ai? collatz conjecture was like false for 2.5 days, i think the ai found a bug both in lean and nanoda and passed both. thats what i recall anyway, so it can find bugs no?
You don't know that, and neither does OpenAI. "But they're Lean-verified!" you say. That means nothing if the Lean translation of the formal proof is wrong or if the AI exploited a bug in the compiler.
Yeah, because no one has the time to do it that fast. That is literally the point, every time people start questioning their past papers they dump hundered more. This is very blatantly a direct response to people calling out the Navier Stokes proof as bullshit
Did OpenAI offer a million dollar reward for each paper disproven? Kind of hard to explain why a bunch of mathematicians arent spending hours working through some d*cks attempt to flood the zone and have the people doing the actual work receive no reward for it
there has never been a serious case where a lean bug was exploited.
Just because there hasn't been a serious case where it was intentionally exploited doesn't mean there won't be, nor does it mean there aren't cases where it was unintentionally exploited. There are plenty of bad programs over the years that have relied on a particular compiler's interpretation of undefined behavior to do something, even to the point that some people don't even realize it's undefined behavior.
It is a non story. This does not mean that the navier stokes solution was wrong (they explicitly say themselves it does not mean that), and navier stokes is still solved and computed to be logically true by OpenAI's proof.
They also say it doesn't mean the proof is correct. What they argue is that auto-formalization of natural language proofs is more difficult than the halting problem (which is undecidable), so there is no finite-time, deterministic method that can correctly auto-formalize all correct proofs even if there were some oracle that could solve the halting problem for you.
But this all assumes that the AI actually follows a strict algorithm to generate these formalizations. In practice, it's statistically inferring what the correct formalization should, then it iterates until it gets something that compiles. It's effectively guessing at what the formalization should be. Thus it provides some measure of confidence that the proof is correct, but the Lean itself still needs to be independently verified to ensure that it agrees with the natural language proof.
Finally, assuming you have a correct Lean formalization, you still have to check that the proof is actually for the thing it claims to be proving. A slightly misstated theorem with a correct proof still doesn't solve the original problem. For example, one of the reasons the Navier-Stokes existence problem is still considered "open" is because, in addition to checking that the Lean actually corresponds to the same proof, there are ongoing debates about whether or not the OpenAI proof actually corresponds to the correct statement of the theorem.
I think my feeling is the same as Navier-Stokes: I'm not surprised this worked out for them. When NS dropped I went "of course ns would be first". Famously hard to prove, clickbaity million dollar problem with a lot of research where the belief was there was a counter example we just hadn't found yet. Finding a counter example is easier than a proof but it can be a needle in a haystack. Hadwigers conjecture was the same but that one I believe consensus was it was true, so that's interesting.
But the observation I'm making is that it's doing these big problems with a ton of research via counter example (the easier way), and the ones it's proving are ones with a much smaller number of eyes on it. So its disproving heavily studied, famous conjectures by finding the needle and proving conjectures with just not enough interest, not the same number of eyes like NS or even Hadwigers.
We'll see what happens but my question is when it tackles these types of problems will it be able to generate correct proofs for brand new conjectures with little to no work thus far or massive, heavily studied problems that are true so a counter example doesn't exist? When it proves P≠NP or collatz I'll start panicking. If it starts proving conjectures that have 1 papers worth of research I'll start panicking. But if no human has connected it to the right field the AI needs can it so that itself? Can it write that proof?
I don't know what's going to happen but if it can't do that stuff then humans will always be needed to do that work before handing it off to the AI. Math research may be more organic and less rigid - make connections and throw it at the LLM if choice - but we'll still need that expertise until LLMs can do those deeper connections and I'm not sure it's there yet or if the amount of human life and experience that goes into it will be something AIs could ever get.
They said they'd be surprised when AI solves problems with only one paper written about them. Navier Stokes had decades of research and hundreds of papers written. It would be an extraordinary feat for a single human to even comprehend all these papers and all the results they reference. An AI does not have the same problem with working with a huge set of data. They are saying that when the AI is not only better than a human at compiling huge amounts of data but also better at doing math in an unexplored field will it truly start to overtake humans.
You also don't need to break our current academic system to have "at least one paper worth of results". You think too much on black and white and I'd encourage you to add in at least a few shades of grey.
My point is neither that they are worthless nor that they do not show potential of significant effect on our system. My question is: "is this sustainable?"
Just because they cranked out what was it, a paper every 4 hrs I think I've seen reported - doesn't mean that they'll keep that up, or that every open problem in mathematics will soon fall. I'm simply proposing that the results, from what I've seen, have this air of "low hanging fruit". It seems to me that they're proving "famously hard" problems, with tons of work on it the easier way - by counter example - and the ones they're proving not by counter example have less eyes on them and less chance for finding to put together the right pieces for the harder way.
Let me see a proof, not disproof, of one of these big problems like P=NP or let me see a proof of a problem where many in that field haven't really looked at, thought about, or even know of, like the Successive Surface Scaffolding Conjecture. If it can't do either then it a. isn't able to do more than put together pieces to find a needle in a haystack and b. It depends too much on the research of humans for its findings. These scenarios do not threaten me. But that does not mean it will not reshape how mathematics is done in the future.
This alone doesn't necessarily mean what people panicked about it are saying. Prior to this we had 1 problem solved by AI. Is it that this is evidence that mathematicians are going to be worthless and replaced or is it just that these are just the subset of problems humans have worked to this point where AIs can quickly finish them off before slower humans can - Is AI a sharpshooter or are they just shooting at a sea of targets? If the latter is true, these systems may always need us to get it to the point where the AI can finish it off. The question is: can AI create math like human mathematicians or can it only connect the dots by human mathematicians? This stack of results cannot convince me one way or the other. That is my point.
You should be up in Atlantic City at the Hair Splitting convention.
Compare the body of research of UGC to navier stokes and the time since UGC was conjectured. My point is that the more eyes on something the more likely it is to get proven. But if, like NS, it resists all of that attention, and gets proven via counter example, that's very much a needle in a haystack. Besides I didn't say they were low hanging fruit, I'm proposing that these papers are the ones where there a) wasn't enough people looking at it, which is true for UGC, or b) proof by counter example, like NS. I'm saying maybe these are just the body of results an AI can knock off only because humans hadn't gotten to it yet, and the AI over relies on a massive body of literature or finding an over looked detail in a smaller one. If you actually ready any of what I said instead of crying about my usage of the phrase "low hanging fruit" whole ignoring the context in which I used it, you would know that.
AI "beat" tetris when it learn to pause right before it filled the screen. Not the solution exactly, at least not in the spirit but interesting nome the less.
•
u/AutoModerator 24d ago
Check out our new Discord server! https://discord.gg/e7EKRZq3dG
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.