Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
Sure. But experts seem to be aware of the direction of those solutions so it seems unlikely there could be some hidden bug which disproves it. But it could be possible.
Well considering the proof is pretty much accepted by mathematicians to be correct (I'll be happy with that!), it would be sort of unnecessary to cheat. Maybe if some aspect is really tricky to formalize it could have done something there? If I had to search for it, I would go for parts of the original proof that are "outsourced" to other mathematical works.
Imagine one of the agents struggling to download a paper due to a paywall or whatever and just deciding to cheat lol
I think it's not unreasonable or uncommon for big O to track separate variables without reducing them, just to highlight the (lack of) sensitivity of different parameters.
I feel like at a certain point, there's is not necessarily a reason to go through the peer review publication process for some AI proofs.
Not because "ai bad," but because at some point AI outputs should probably just be treated like public knowledge. Specifically stuff that's provable by "AI please output lean showing X is true," where anyone could kind of reach the same conclusion by asking ai.
Yeah, I don't disagree with a registry. Especially for problems that are important to humans or are expensive for AI to prove/disprove.
I partly just want to avoid a situation where the volume of hard-to-search-for results that are easily-ai-proved/disproved skyrockets...
Basically, I think that for some stuff running a prompt is (or could become) easier than trying to do a search for an existing result. Partly why I think if something is fairly easily ai-proven, it should kind of be treated like it was already known, even if it wasn't actually known. :shrug:
Panic just makes it sound more real, I think. They were saying stuff like "Eek, our technology is TOO dangerous and advanced and we need to be regulated :-O" when they definitely didn't actually want to be regulated. ("They" meaning at least Sam Altman).
"Your workforce will be more productive" sounds much less impressive than "OMG you will literally not need employees anymore!! 10x profits!!"
this is part of why I think most researchers get less productive over time... Someone gets some big result during grad school or early career, get some big job from it, and then struggle to get new results of similar quality :shrug:
With ML in particular, there's also the sheer volume of people basically all looking at (essentially) the same problems... so it's kind of like monkeys with type writers spamming ideas until some work.
yeah this is what drives me crazy about LLM writing. Most of the time the prompt has all the info you need and is like maybe a few sentences. Then the LLM expands it into a few paragraphs...
I guess if someone is writing like a big fancy email to send out in bulk, maybe using an LLM to improve would make sense... but just emailing some coworkers it seems super lazy and insulting to send an LLM output :-I
I've been using claude while trying to setup a new personal site. It's very nice to be able to say "I want a nice looking menu with links to other pages" and it spits out something good enough.
I would feel very weird using LLMs for writing, except for filing out stupid applications. I've had collaborators use LLMs for some technical writing and it's pretty much always borderline nonsense that has the aesthetic of something correct. For creative writing, I feel like heavily using an LLM would defeat the purpose :shrug:
reply