[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.