15 citations · 27 across the 7 of their papers we have counts for
5 papers · 1 filter
Formalising the -principle and sphere eversion
Patrick Massot, Floris van Doorn, Oliver Nash
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existen…
Designing a general library for convolutions
Floris van Doorn
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applica…
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…
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…
Higher Groups in Homotopy Type Theory
Ulrik Buchholtz, Floris van Doorn, Egbert Rijke
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a point…