Comment by scapp

> Last time I checked there was still no formal version of Cantor's diagonalization argument.

Formalization? Like a computer checked proof?

Lean: https://leanprover-community.github.io/mathlib_docs/logic/fu...

Coq: https://github.com/bmsherman/finite/blob/63706fa4898aa05296c...

Isabelle: https://isabelle.in.tum.de/website-Isabelle2009-2/dist/libra...