Comment by auggierose

How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.