In formal settings you’d call me Synthesist.
—Peter Watts, Blindsight (2006)
On that angle, it could be further argued that humans are biased towards 'readable' proofs and that there are many undiscovered 'unreadable' proofs that we simply have no way of obtaining without automation of some kind.
Anyway I assume there are volumes already written on this subject...
The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.
I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.
A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it.
Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied.
Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.
Maybe not directly. But if AlphaProof managed to prove the Riemann hypothesis, I bet it wouldn't be long before human mathematicians had managed to decipher the proof and explain it in a way that other mathematicians found useful. It's just a lot easier to re-explain something that other people have already proved, rather than proving it yourself.
In fact, looking at chess engines tells us that sometimes (though not always) brute-force calculation of many possibilities gives us better moves. In the same way some true statements might just be an exhaustive calculation.
Perhaps the four color theorem is the most famous example of a proof that has lacked (still lacks) a lot of useful lemmas in relation to its length: https://en.wikipedia.org/wiki/Four_color_theorem
I hope we do get some famous theorems proved by computers so that we can see whether it's enlightening to humans. I am quite curious whether my intuition is correct and it is a shame to think I might never know....
Then how would anyone be sure it isn't wrong?
It was great that while Goldston and Yıldırım were wrong, their work proved to be useful. A lot of people are glad that Riemann (and Fermat) didn't their problems!
Of course, it is possible that clever users could tease useful information out of the black box truth oracle. Perhaps by modifying the statement of the conjecture and checking each modification, they could discover some parts of the structure of the problem, which would help inspire a useful proof. Furthermore, it would be helpful to never again waste time trying to prove a false conjecture.