Problem 22 "The Non-Denumerability of the Continuum" of 100 on this list already has a formalisation and proof thanks to the awesome people at NASA.