Comment by OxO4
1 day ago
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.
1. Well, mathematics isn't other industries
2. It really doesn't work well in other industries either.
My point is that the AI agents are not trying things at random.