> and for arithmetical statements, the system must necessarily be sound
Why do you say this? The AI doesn't know or care about soundness. Probably it has mathematical intuition that makes unsound assumptions, like human mathematicians do.
> How likely are each of these outcomes?
I think they'll all be true to a certain extent, just as they are for human mathematicians. There will probably be certain classes of extremely long proofs that the AI has no trouble discovering (because they have some kind of structure, just not structure that can be expressed in ZFC), certain truths that the AI makes an intuitive leap to despite not being able to prove them in ZFC (just as human mathematicians do), and certain short statements that the AI cannot prove one way or another (like Goldbach or twin primes or what have you, again, just as human mathematicians can't).
Why do you say this? The AI doesn't know or care about soundness. Probably it has mathematical intuition that makes unsound assumptions, like human mathematicians do.
> How likely are each of these outcomes?
I think they'll all be true to a certain extent, just as they are for human mathematicians. There will probably be certain classes of extremely long proofs that the AI has no trouble discovering (because they have some kind of structure, just not structure that can be expressed in ZFC), certain truths that the AI makes an intuitive leap to despite not being able to prove them in ZFC (just as human mathematicians do), and certain short statements that the AI cannot prove one way or another (like Goldbach or twin primes or what have you, again, just as human mathematicians can't).