It'll just be telling you what the data it ingested claims. Not what is necessarily true. It's as subject to garbage in, garbage out as anything, and you don't know what it's actually trained on.
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
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
Adding a G to the UI is 'giving the finger' to their old players? When they include support for ASCII-like tilesets so you can play the exact same way? "Gamers" are the most entitled people on earth, I swear
Totally agree that it's just a proxy for people's feelings on AI, but my Lobster Jesus is much more important to me than a Netflix show! All of the datacenter usage (for inference) is just serving something people want. Time has already shown that the datacenter for training is also just creating something people want.
> All of the datacenter usage (for inference) is just serving something people want.
I agree with this in principle, but I wonder how asymmetric the usage is. When I hear about developers dropping $200/mo (subsidized!) on AI coding, and having multiple agents on supergigaultramax effort churning on stuff for hours... Versus your average person maybe asking a few chatgpt questions every day or week... IDK.
Like others have said, yes, OpenAI probably isn't literally going to sell you more than $200 of electricity for $200/mo. But data centers get industrial rates, and $200 of power is still a decent bit of power just to be churning out slop! (It's about a monthly home bill and EV charging cost combined) And some companies spend way more than that on API pricing for tokens... It's just hard to get a handle on where the usage is actually going.
I just wish we could pass a common sense law to require them all to build renewables. It's literally electricity, it's the easiest energy to decarbonize.
i think this sentiment comes from a deep misunderstanding of how our modern society is the product of transitive satisfaction of wants. the developers churning out agent work on supergigaultramax effort are fulfilling the transitive preferences of people like supply chain managers, etc. who are in turn fulfilling the transitive preferences of a school teacher for cheap groceries, who are in turn....
This is how economies work and the alternative strategy of enumerating morally correct wants/needs and assigning the correct price from on-high has been a demonstrable failure. It is a cognitive failure of humanity that this strategy is so intuitively appealing to us.
> the developers churning out agent work on supergigaultramax effort are fulfilling the transitive preferences of people like supply chain managers, etc.
Sure, but that's the crux of it all, isn't it. Are they? And are they doing it that much better than before?
I'm far from an AI coding skeptic at this point, the stuff works, and I use it, but I think it's fair to ask whether it's worth burning a middle class home's amount of electricity to spit out CRUD apps and web frontends a bit faster. As many have pointed out, we've still yet to see some kind of huge productivity increase in society at large, or even some particularly revolutionary new app or whatever.
On some level it's people's money and they can spend it how they want, but people get criticized for unnecessary waste of resources all the time.
I think people should be allowed to do things, generally. If it's not worth it, the people doing it will go out of business (and quickly, at these prices). I think it is likely more worth it than you realize.
We're not talking about criticizing, we're talking about bans.
> If it's not worth it, the people doing it will go out of business
In general I agree (and many environmentalists and such undervalue the fact that environmental waste often correlates with wasted money), but I don't think this is a reliable principle. You can always brute force your way though problems, sometimes it's cheaper that way, doesn't mean it's not wasteful.
We are also assuming that economic value means something is good for society. A lot of money is made off of social media, ads, gambling apps, clearly there's demand for it. I don't think that means we can say all those things are good, just off demand alone.
I'm not really talking about banning anything, I just think it should be asked whether this stuff is worth it. We're just two guys on the Internet, it doesn't really matter at the end of the day.
I think that low externality things people are willing to pay for should be presumptively allowed unless there is strong reason otherwise. We are much too involved in the 'legislating individual activities' and not nearly enough in the 'tax wealth and redistribute' side of things.
> We're just two guys on the Internet, it doesn't really matter at the end of the day.
Post-2020, the internet is real life. Internet native thought has proven to be a powerful force in the physical world. I remember laughing at the absurdity of 4chan posters in high school. I will not make the mistake of taking internet ideology lightly again.
It's also a cognitive failure of humanity to assume the free market is only guided by the invisible hand of demand and supply, if only government and moralists would get out of the way.
> the developers churning out agent work on supergigaultramax effort are fulfilling the transitive preferences of people like supply chain managers, etc. who are in turn fulfilling the transitive preferences of a school teacher for cheap groceries, who are in turn....
This ceased to be true lomg time ago. AI datacenters are not related to that chain.
For that matter, tech is not about satisfying a bunch of small customers either. Enshittification would not be a thing if it was.
>the developers churning out agent work on supergigaultramax effort are fulfilling the transitive preferences of people like supply chain managers, etc.
Some of them are doing this at their jobs, but there are also tons of people pushing slop to open-source projects, vibe coding useless or redundant apps, etc.
reply