Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable
Author: Jørgen Villadsen
Paper Information
| Title: | Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable |
| Authors: | Jørgen Villadsen |
| Proceedings: | ThEdu Extended Abstracts |
| Editors: | Pedro Quaresma and Walther Neuper |
| Keywords: | Isabelle Proof Assistant, Uncountability, Real Numbers |
| Abstract: | ABSTRACT. 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. |
| Pages: | 6 |
| Talk: | Jul 18 14:30 (Session 127M) |
| Paper: |  |