kai-e.github.io
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.