To ask that question suggests you are unfamiliar with the difference between arithmetic (which computers are good at) and pure mathematics (which is like metaprogramming combined with formal methods, and Gödel's incompleteness theorem is worse than the Halting problem)?
Simply put: For the same reason computers have not already solved all problems in mathematics.
More concretely:
Consider the Collatz conjecture. It's a very simple rule to write down:
Take some positive integer: If the number is even, divide it by two; otherwise triple it and add one. With enough repetition, do all positive integers converge to 1?
Trivial to write a program to test numbers starting at 1 and going up. We know it holds up to at least 2.36e21 (according to Wikipedia), but to prove it is true with such a program requires testing all of the infinite set of positive integers.
But you may notice some things about the rules, that they suggest a subset of numbers will trivially always converge to 1, so that you don't need to even test them: any integer 2^n where n is also a positive integer.
You may find other easy wins, or ways to simplify the test, e.g. once you know the numbers up to m will converge to 1, you can terminate your loop early if you test m+1 and it ever has an intermediate value less than or equal to m. You can combine that with applying one of the rules in reverse, and know that all even numbers between m and 2m will on their first move be halved, making them smaller than m, which means you know they'll eventually converge.
But actually proving this is fully general? Nobody knows. You can't just throw arithmetic at the problem directly, you have to figure out patterns that would let you prove that it always holds, no matter what.
Or, you may find many such patterns and directly calculate some number not in any of them, to find one which doesn't converge to 1.