551–560 of 642 posts
Earlier quoted context omitted.
Not if it's lean-verified.
Didn't some of the recent proofs exploited a couple of blind spots of lean, and they were invalidated? Edit: Yup. A bug report to Lean was disguised as a "Collatz" proof in a humorous way. Links below. - https://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943
At some point we will lose track of all the ai discoveries that are worth remembering. Academia with the publication system had a way of retrieving old discoveries and build upon them. If my LLM session found something groundbreaking in between the billion tokens it produced, how would you ever know?
I’m being somewhat harsh here but come on - human endeavors are messy and it’s surprising how much our egos are getting bruised here over seeing the value of these tools
Dont get me wrong Also, there’s no AI Utopia coming this is it guys, were stuck with oligarch Tech Bro funded AI and big funded Govt AI so forget any egalitarian motives- we have to fight for our rights from other humans as always as well but AI as a technology in itself being able to truly solve unsolved intellectual problems is still a boon for society - who cares who gets credit?
Earlier quoted context omitted.
> It's a bit like a tree falling in a forest. If an LLM proves a theorem but no one understands it, did it make a sound? But in future most proofs will be for consumption by other AI models in the pursuit of yet other proofs. It's kind of surprising so many mathematicians act surprised by this given this was clearly where automated proof assistants would lead. I guess they assumed they'd always be the ones guiding th…
> But in future most proofs will be for consumption by other AI models in the pursuit of yet other proofs. What is the purpose of that? Its like art being produced for AI to consume. What is gained from that?
I understand this stance and where they are coming from, but I can't help but think this sounds very analogous to engineers' arguments against AI-assisted and vibe-coding, especially with regard to cognitive debt. Yet the software industry is plowing ahead, reportedly pushing mountains of unreviewed code to Prod, and the world hasn't ended. Of course, nobody's really comfortable with it, so this is also a forcing fun…
Yes, this has gone so well
Earlier quoted context omitted.
Not if it's lean-verified.
Didn't some of the recent proofs exploited a couple of blind spots of lean, and they were invalidated? Edit: Yup. A bug report to Lean was disguised as a "Collatz" proof in a humorous way. Links below. - https://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943
Earlier quoted context omitted.
Didn't some of the recent proofs exploited a couple of blind spots of lean, and they were invalidated? Edit: Yup. A bug report to Lean was disguised as a "Collatz" proof in a humorous way. Links below. - https://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943
I don't know ... do you have a reference?
This sounds a lot to me like people in the 90's complaining that computers were destroying chess. Thirty years later, chess is more popular than it ever was, and chess players are better than they ever have been. I wouldn't be surprised if there are now more chess books now than there ever have been. Furthermore, it turns out that a lot of chess books written before computers were just wrong about a lot of things. It…
Well, chess is a sport where humans are supposed to compete. But math, programming, science are mostly not, and AI might affect economy, careers, etc.