15 citations · 38 across the 8 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.LO2021
Formalized Haar Measure
Floris van Doorn
We describe the formalization of the existence and uniqueness of Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups…
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…