2 is definitely true. 3 is much more interesting and likely true but even saying it takes us into deep philosophical waters.
If every true theorem had a proof in a computationally bounded length the halting problem would be solvable. So the AI can't find some of those proofs.
The reason I say 3 is deep is that ultimately our foundational reasons to assume ZFC+the bits we need for logic come from philosohical groundings and not everyone accepts the same ones. Ultrafinitists and large cardinal theorists are both kinds of people I've met.
My understanding is that no model-dependent theorem of ZFC or its extensions (e.g., ZFC+CH, ZFC+¬CH) provides any insight into the behavior of Turing machines. If our goal is to invent an algorithm that finds better algorithms, then the philosophical angle is irrelevant. For computational purposes, we would only care about new axioms independent of ZFC if they allow us to prove additional Turing machine configurations as non-halting.
If every true theorem had a proof in a computationally bounded length the halting problem would be solvable. So the AI can't find some of those proofs.
The reason I say 3 is deep is that ultimately our foundational reasons to assume ZFC+the bits we need for logic come from philosohical groundings and not everyone accepts the same ones. Ultrafinitists and large cardinal theorists are both kinds of people I've met.