“ [L]et me make the bold suggestion that perhaps in a few decades we shall see what nonhuman mathematics looks like. I am not predicting the imminent arrival of little green men from outer space, but simply the invasion of mathematics by computers. Since the human brain is a sort of natural computer, I see no reason why the artificial variety could not perform better in the specialized task of doing mathematical research. My guess is that, within fifty or a hundred years (or it might be one hundred and fifty) computers will successfully compete with the human brain in doing mathematics, and that their mathematical style will be rather different from ours. Fairly long computational verifications (numerical or combinatorial) will not bother them at all, and this should lead not just to different sorts of proofs but more importantly to different sorts of theorems being proved.
”
”
