I agree with the concerns on the false dichotomy between theoretical computer science and mathematics, but from the mathematician's perspective I think there's another issue not being discussed due to the typical CS obsession over automated proof systems.
Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of course the point is also to be correct, but somehow communicating insight takes priority. Relying on large bodies of latent knowledge, and omitting details, is an effective way to do that. Allowing for occasional mistakes is okay, because mathematics as a whole is fault tolerant (or at least, history gives evidence to that claim).
Lamport's field is a bit different, because there they study distributed protocols with the intent of creating value in the real world. So when they prove a theorem, they're not just proving a theorem to gain understanding about something, they're proving a theorem so they can improve the security or fault-tolerance (or whatever else) of some real system. Writing down a 200+ page TLA proof is measurably worth the investment because the users of their work (applied computer scientists and engineers) want error-free theorems and a clean CS literature much more than they want insight.
For mathematicians communicating to other mathematicians, a two-paragraph argument that is convincing and omits the details (that one can verify on their own) is much more valuable. I'm not trying to make a value judgement either way, just trying to explain the culture of math proofs and why I think something like TLA+ will never catch on among mainstream mathematicians. You might say it's mathematicians defending their job security, but it's also simply that mathematicians like exploring and inventing and hearing creative proofs and perspectives. Deferring things to computers removes the a-ha moment.
[Edit] And the idea that somehow high school students and undergraduates will magically start reading and understanding proofs because we write them using TLA+ is a joke.