Comment by monktastic1
12 hours ago
But this oracle doesn't just say true / false. It also gives a proof. That makes it much less exciting (not to mention beneficial for your career) to find another one (or even worse, the same one).
12 hours ago
But this oracle doesn't just say true / false. It also gives a proof. That makes it much less exciting (not to mention beneficial for your career) to find another one (or even worse, the same one).
The "proof" is merely an appeal (unreadable program) submitted to a different oracle (Lean).
What do u think lean is? That's like saying a program that works, is inscrutable because it appeals to the oracle of "code test cases" to prove itself correct.
You're either being intentionally obtuse, or unintentionally ignorant.
Have you tried to read the Lean proofs produced for any of the recent high-profile results? They're extremely long, terribly structured, and don't indicate which parts are restating known results from literature and which are unique to the proof at hand. That's what makes them inscrutable.
It's similar to Mochizuki claiming to have proved the ABC conjecture, with a proof depending on ideas developed over a large number of obscure papers, that required mathematicians to spend a lot of time before they felt they understood it well enough to point out flaws.
If AI solves all famous open problems and the non-famous ones, too, without advances in the readability of their output, there'll still be some work to do to digest and rearrange the proofs for human consumption. During that process, the mathematician may well get some new ideas...
1 reply →