## 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.

for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory.

Original language | English |
---|---|

Publication date | 2018 |

Number of pages | 6 |

Publication status | Published - 2018 |

Event | International Workshop on Theorem proving components for Educational software - Oxford , United Kingdom Duration: 18 Jul 2018 → 18 Jul 2018 http://www.uc.pt/en/congressos/thedu/thedu18/programme |

### Conference

Conference | International Workshop on Theorem proving components for Educational software |
---|---|

Country | United Kingdom |

City | Oxford |

Period | 18/07/2018 → 18/07/2018 |

Internet address |