Comment by walrus

Computers are used in (some parts of) math for exploration, but not so much when it comes to conjectures and proofs. In fact, I would argue that making conjectures is a distinctly human activity: it requires you to decide if something is 'interesting' or not.

On the proving side, there is some software such as Coq or Agda that provide heuristics, but you won't find the typical mathematician using them. In many proofs, things are said to be 'obvious' or 'follow clearly' from a previous statement. A mathematician (trained in the relevant area of math) can fill in those parts with their intuition, but a computer can't. That often makes a computer-readable proof prohibitively long compared to a human-readable one.

That's not to say mathematicians shouldn't learn to use that sort of software. The only way to fill in those 'obvious' or 'follows clearly' parts is to build a large library of arguments that can fill them in.