Conference paper
Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable
We present a new succinct proof of the uncountability of the real numbers – optimized for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory.
Language: | English |
---|---|
Year: | 2018 |
Proceedings: | International Workshop on Theorem proving components for Educational software |
Types: | Conference paper |
ORCIDs: | Villadsen, Jørgen |