Comment by soVeryTired
1 day ago
Or maybe the PhD impersonator discovered a soundness bug in a component of Lean and was able to exploit it.
With no humans able to understand the proofs the impersonator has produced, there's no way of knowing.
1 day ago
Or maybe the PhD impersonator discovered a soundness bug in a component of Lean and was able to exploit it.
With no humans able to understand the proofs the impersonator has produced, there's no way of knowing.
There are many independent implementations of Lean's proof checker:
https://arena.lean-lang.org/
It's highly implausible that the same bug is present in all of them.
Is that true? I'm actually asking because all the ones that I have seen mentioned from the arena were generated with Claude and I just checked a few random ones and they all have commits by Claude.
I don't know how much was created by LLMs but can you still call these independent implementations?
Yes? Very little about Claude is deterministic. If given the same sufficiently complicated problem, but via slightly different input prompts, it can generate entirely different code. It would be shocking if they all had a single shared bug.
2 replies →
If the AI had found a bug, I expect it using the bug to prove everithing and geting 700 pdf per week https://xkcd.com/704/
This is true of literally any proof of sufficient complexity, human-authored or otherwise.
It takes time to convey the core ideas. It takes time for other mathematicians to come up to speed on the new techniques and approaches or the novel combinations of existing ones.
The actual experts in this field have asked for the argument to be explained to them, and are now at the point where they believe this is plausible. Another person in this thread has produced a Lean proof and presumably is not trying to pull a fast one on us by exploiting a bug in the solver.
TL;DR chill bro.