15 citations · 27 across the 6 of their papers we have counts for
Showing math.LOShow all
2 papers · 1 filter
math.LO2021★ 10 cited
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han, Floris van Doorn
We describe a formal proof of the independence of the continuum hypothesis () in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for bo…
math.LO2015
Propositional Calculus in Coq
Floris van Doorn
I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction…