Comment by p-e-w
1 day ago
Now imagine that PhD “impersonator” has, in the past few months, made more demonstrable progress in mathematics than anyone in history.
I think that would change the conclusion of the argument a little.
1 day ago
Now imagine that PhD “impersonator” has, in the past few months, made more demonstrable progress in mathematics than anyone in history.
I think that would change the conclusion of the argument a little.
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?
3 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.
More realistically, that impersonator has created lots of output, and the correct ones are selectively publicized (and few particularly interesting bad answers).
Yes from a social proof perspective.. not really from an objective truth seeking perspective, the best liar tell truths 99% of the time.
Do you really believe Open AI made more progress in math than any of the human predecessors? Come on.
Galois had built modern algebra before dying at 20. What agents did so far is flash in a pan.
Wait and see when _they_ are 20 years old!
[dead]
He should have written longer letters and duelled less.
> Galois had built modern algebra before dying at 20.
No he hadn’t. You are clearly consuming mathematics through a pop culture lens.
[dead]
The recent progress does not imply that the "impersonator" has a deep understanding of mathematics. By formalizing a problem in Lean, constructing the proof is essentially a complex search. Because Lean is the arbitrator of correctness, the "impersonator" can make as many mistakes as they want until they find a solution that passes the checker. That is very different from checking a paper for correctness.
complex searches are quite valuable in mathematics. For example, Maryna Viazovska's fields medal was for finding the right gadget (roughly, a complex search) to prove optimality results in sphere packings.
Right, my comment was not about its usefulness. I was merely pointing out that those results do not necessarily imply any kind of actual understanding.
that's a hard cope. You think humans don't make thousands of mistakes to come up with something good?
Of course humans make mistakes, but (outside of Lean at least) they attempt to solve it with experience, understanding, and a certain amount of creativity instead of mashing things together until something works out.
Good luck writing a Lean proof of a nontrivial theorem by giving a keyboard to a thousand coke-fueled monkeys. If only it was that easy.
To an extent, that is what automated theorem provers (e.g., SAT/SMT solvers) do quite successfully. The monkeys have very good heuristics and avoid going down unnecessary paths, but they are still monkeys. Similarly, AI might be very good at recognizing patterns (which is very useful!), but doesn't necessarily demonstrate any kind of real understanding.
Strange to be against this when it works so well in other industries.
2 replies →