As someone whose research currently consists of proving things in proof checkers, I can confirm they are more complicated than LaTeX.
At one point, I had to prove n / 15 + n / 4 + (2 * n / 3 + 1) <= n, for positive n. Seems simple right? But first you have to multiply by 60 so that you're working over actual naturals. But then you have to contend with the fact that n / 15 * 15 <= n itself needs proof (they're not just equal, since n / 15 actually represents the floor or that quotient). Automatic tactics that simplify things for you help some, but it still ends up being a good 8 lines of code for such a trivial statement. When things like this can be handled fully automatically, then it will be ready for mainstream use.
At one point, I had to prove n / 15 + n / 4 + (2 * n / 3 + 1) <= n, for positive n. Seems simple right? But first you have to multiply by 60 so that you're working over actual naturals. But then you have to contend with the fact that n / 15 * 15 <= n itself needs proof (they're not just equal, since n / 15 actually represents the floor or that quotient). Automatic tactics that simplify things for you help some, but it still ends up being a good 8 lines of code for such a trivial statement. When things like this can be handled fully automatically, then it will be ready for mainstream use.
It is fun to fight the proof checker though! :)