You have asked the bot to summarize the proof for you in natural-language, but you know that the bot can easily trick you into accepting the proof.
I didn’t fully get this point. Sure, there definitely are gigantic computer-generated proofs out there, the most famous being the proof of Four Color Theorem (which some mathematicians in the 80s rejected precisely because it was infeasible to check by hand); I accept that our bot could produce a truly huge blob.
On the other hand, optimizing a bogus proof for human validation sounds even more difficult than just search for a correct proof. To search for correct proofs you just need to know math; to search for plausible bogus proof you need to know math and how human mathematicians typically validate proofs. Are we just assuming to work with AGI here?
The proof need not be bogus, it can be a long valid proof but since you are describing the problem in natural language, the proof generated by the AGI need not be for the problem that you described.
I didn’t fully get this point. Sure, there definitely are gigantic computer-generated proofs out there, the most famous being the proof of Four Color Theorem (which some mathematicians in the 80s rejected precisely because it was infeasible to check by hand); I accept that our bot could produce a truly huge blob.
On the other hand, optimizing a bogus proof for human validation sounds even more difficult than just search for a correct proof. To search for correct proofs you just need to know math; to search for plausible bogus proof you need to know math and how human mathematicians typically validate proofs. Are we just assuming to work with AGI here?
The proof need not be bogus, it can be a long valid proof but since you are describing the problem in natural language, the proof generated by the AGI need not be for the problem that you described.