The issue is that we would like to assume that the genie is smart (think AGI) but not omniscient. I expect that if a hundred smart humans worked for a hundred years they could prove the Riemann hypothesis. I very much doubt that they could prove they had found the shortest proof.
Agreed
(in fact in general, statements like that can undecidable quickly)
Surely “check all the proofs in order” is an algorithmic way to determine that a given proof is the shortest?
All I’m looking for is the shortest proof the AI can manage to find (which is why it is extremely subtle to formalize what I mean by “the AI has no influence”).
Then we agree with each other, but you might want to edit your post to reflect this. Asking “is there a proof of length 2?” seems to indicate my interpretation rather than “can you find a proof of length 2?”.
Agreed
Surely “check all the proofs in order” is an algorithmic way to determine that a given proof is the shortest?
Then we agree with each other, but you might want to edit your post to reflect this. Asking “is there a proof of length 2?” seems to indicate my interpretation rather than “can you find a proof of length 2?”.