Another question, do you use Cantor-style diagonalization for the fixed-point theorem? Apparently this is the case for the standard proof of incompleteness, as explained here, though this paper goes over my head: https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kl...

The reason why I'm asking is that Cantor used diagonalization in his famous "diagonal argument" for the real numbers being uncountable. Some people found this argument unconvincing, because it relied on perhaps questionable assumptions, like the decimal representation of real numbers and that different decimal representations must denote a different real number. But if the diagonal argument (or his earlier powerset argument) could be formalized and checked with Coq, doubts would presumably be removed.

If you think Kleene's recursion theorem and Cantor's diagonalization are the same sort of argument, then I'd say yes.

I don't know if people historically had an issue with Cantor's argument or not. Certainly the modern presentation with decimals can be dicey if you are not careful because, as you note, some real numbers have two representations as decimals, one with repeating 9's and another with repeating 0's. But this issue can be avoided so long as you are careful. e.g convert all non-5's to 5's and convert 5's to 6's, thus staying far away from the dangerous 0/9 zone of digits. The constructed decimal sequence only has 5's and 6's and thus is a real number with a unique decimal representation.

There is no problem with Cantor's argument, and it can easily be formalized. It would be a reasonable exercise to do at some point in an introductory course for proof assistants.