Showing 1–9 of 9 results for author: van Doorn, F

Formalising the $h$-principle and sphere eversion

Authors: Patrick Massot, Floris van Doorn, Oliver Nash

Abstract: 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 existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topo… ▽ More 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 existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his swee** effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured △ Less

Submitted 14 October, 2022; originally announced October 2022.

Comments: 30 pages, submitted to CPP 2023

MSC Class: 68V20; 57R12 ACM Class: F.4.1

Designing a general library for convolutions

Authors: Floris van Doorn

Abstract: 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 applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib. 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 applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib. △ Less

Submitted 14 October, 2022; originally announced October 2022.

Comments: 24 pages, submitted to CPP 2023

MSC Class: 68V20; 42A85; 44A35 ACM Class: F.4.1; G.3

Formalized Haar Measure

Authors: Floris van Doorn

Abstract: 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, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean's mathematical library \textsf{mathlib}, and discuss the construction of product measures and the proo… ▽ More 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, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean's mathematical library \textsf{mathlib}, and discuss the construction of product measures and the proof of Fubini's theorem for the Bochner integral. △ Less

Submitted 4 February, 2021; originally announced February 2021.

Comments: 16 pages (excluding references)

MSC Class: 28C10 ACM Class: F.4.1; G.3

Maintaining a Library of Formal Mathematics

Authors: Floris van Doorn, Gabriel Ebner, Robert Y. Lewis

Abstract: 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 and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied aud… ▽ More 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 and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience. △ Less

Submitted 26 May, 2020; v1 submitted 7 April, 2020; originally announced April 2020.

Comments: To appear in Proceedings of CICM 2020

A formalization of forcing and the unprovability of the continuum hypothesis

Authors: Jesse Michael Han, Floris van Doorn

Abstract: 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 logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space $2^{ω_2 \times ω}$ and formally verify the failu… ▽ More 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 logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space $2^{ω_2 \times ω}$ and formally verify the failure of the continuum hypothesis in the resulting model. △ Less

Submitted 23 April, 2019; originally announced April 2019.

Comments: 19 pages; extended version of a paper submitted to ITP 2019

MSC Class: 03-04; 03E35; 03E40

On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory

Authors: Floris van Doorn

Abstract: The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant. The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant. △ Less

Submitted 31 August, 2018; originally announced August 2018.

Comments: Dissertation, 146 pages

MSC Class: 55T05 (Primary) 55T10; 55T25; 55P20; 03B15; 55U35 (Secondary) ACM Class: F.4.1

Higher Groups in Homotopy Type Theory

Authors: Ulrik Buchholtz, Floris van Doorn, Egbert Rijke

Abstract: 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 pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups an… ▽ More 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 pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant. △ Less

Submitted 12 February, 2018; originally announced February 2018.

MSC Class: 03B15 ACM Class: F.4.1

Homotopy Type Theory in Lean

Authors: Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz

Abstract: We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods. We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods. △ Less

Submitted 20 September, 2017; v1 submitted 22 April, 2017; originally announced April 2017.

Comments: 17 pages, accepted for ITP 2017

MSC Class: 03B70; 03B15; 55U35

Propositional Calculus in Coq

Authors: Floris van Doorn

Abstract: 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 calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus. 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 calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus. △ Less

Submitted 31 March, 2015; v1 submitted 30 March, 2015; originally announced March 2015.

Comments: 11 pages, project for 2014 Proof Theory class at CMU. Added ancillary files (Coq source files) in this version