Diagonalization in formal mathematics (2020)