15 citations · 16 across the 3 of their papers we have counts for
3 papers
cs.PL2020★ 15 cited
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…
cs.LO2019★ 1 cited
A formalization of forcing and the unprovability of the continuum hypothesis
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…
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…