Ah but normal math is a social compact in a way that computer-aided proofs are not. Very few handwritten proofs are actually written down in detail, and there a

Ah but normal math is a social compact in a way that computer-aided proofs are not. Very few handwritten proofs are actually written down in detail, and there are various cases where attempting to do so actually failed or required new work to actually close the gap.