Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

DOI10.1007/978-3-031-16681-5_6arXiv2205.03159OpenAlexW4296118504MaRDI QIDQ6159370

Lawrence Charles Paulson

Publication date: 2 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2205.03159

zbMATH Keywords

set theorycontinuum hypothesiscomplex analysisformalisation of mathematicsIsabelleErdős

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Related Items (2)

Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ The formal verification of the ctm approach to forcing

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Set theory. An introduction to independence proofs
• Isabelle/HOL. A proof assistant for higher-order logic
• The foundation of a generic theorem prover
• An interpolation problem associated with the continuum hypothesis
• Partizan Games in Isabelle/HOLZF
• Proofs from THE BOOK
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Formalization of Forcing in Isabelle/ZF
• Formalizing Ordinal Partition Relations Using Isabelle/HOL
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice

This page was built for publication: Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis