Even if there are some branches of mathematics that will be affected by computers, at the end of the day, there will still have to be someone who does the conjecturing, someone with enough knowledge to pose the question to the computer.
Basically, you hop up a level (go meta). Instead of working with the extremely large numbers or sets, you symbolically manipulate statements about them.
I'll repeat what szany and xyzzy123 mentioned: you work at a level of abstraction where infinite data structures are represented symbolically with enough definitional scaffolding to allow proofs to go through.
In a sense, a properly typed program provides a proof of some theorem over infinite data structures. For instance, an instance of a tree (in generic Java) is usually a finite data structure, but the set of all trees representable in Java is infinite. (Handwaving begins) The types prove that certain operations can't happen, like a tree of Strings changing to a tree of Arrays by a node search algorithm, which is a proof about an infinite set.
You're assuming that computers can't handle abstractions.
How does a computer build abstractions on its own?
But it doesn't have to do that, anyway, it can provide means for users to build their own abstractions, abstractions that may be useful for them.