Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof.  Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader.  For Computer Science, a problem of adoption is that proofs are computationally useless (generally).