15 citations · 38 across the 8 of their papers we have counts for
1 paper · 1 filter
Jesse Michael Han, Floris van Doorn
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order lo…