Comment by david-gpu
1 day ago
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.
1 day ago
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.
The same could be said of humans. It is a non-argument.
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.