The ATP/ITP distinction is pretty old and standard. It is more blurred these days when ITPs like Isabelle include ATPs to help making the size of a reasoning step more human-like.

It has not been proven that a computer cannot do math better than a person. Let's say in the future a computer is the first to prove the Riemann Hypothesis. Most people would say that the computer is then better at math than a human.