[zozbot234]

I don't think this is correct. Cantor's diagonal argument follows easily from Lawvere's fixed-point theorem https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theore... and both are quite easy to formalize.

[cubefox]

That seems to be a different proof which implies Cantor's theorem, but not a formalization of Cantor's diagonal argument itself.

[zozbot234]

It is a formalization of Cantor's diagonal argument - in fact, of "diagonal arguments" more generally. See http://arxiv.org/abs/math/0305282 for an expository treatment.

[cubefox]

Thanks, looks interesting.