Floris van Doorn
I am a postdoc at the mathematics department of the University of Pittsburgh, working with Tom Hales on the Formal Abstracts projects. I am a contributor to mathlib, the mathematical library for the Lean Theorem Prover and coauthor of Flypitch, a project where I formally verify the independence of the continuum hypothesis from ZFC together with Jesse Michael Han.
Until summer 2018 I was a Ph.D. student at Carnegie Mellon University under supervision of Jeremy Avigad and Steve Awodey. My dissertation was titled On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory.
I previously studied at the Utrecht University in the Netherlands
where I received a B.Sc. in Mathematics, a B.Sc. in Physics and a M.Sc. in Mathematics. My master
thesis is Explicit convertibility proofs in Pure Type Systems
supervised by Freek Wiedijk at
the Radboud University Nijmegen. I was also trainer for the Dutch
Mathematical Olympiad. Full CV (pdf).
During my Ph.D. I was working on homotopy type theory, although my work in that field has diminished since I started my postdoc.
Homotopy Type Theory (HoTT) is a connection between homotopy theory and type theory, interpreting the basic concepts in the logic of type theory in a geometric way, so that you can interpret many concepts of algebraic topology in it. My main interest here in this field
is synthetic homotopy theory, which is the study of types as spaces in algebraic
topology. My main contribution was to give a synthetic defintion of the Serre Spectral sequence in Lean.
Since the homotopy theoretic definitions are very close to the logical foundations, it
is feasible to formalize many of these results in a proof assistant, without being much more effort than proving these results on paper.
I am also interested in studying higher inductive types, where my main research question was whether it was possible to construct complicated higher inductive types from a simple one, the homotopy pushout.
I formalize mathematical results and develop new tools for the Lean Theorem prover.
I am a contributor to mathlib, and I was the main contributor of
the HoTT library for Lean 2. I was
also the main contributor of the Spectral Sequence
project, where we have formalized the (cohomological) Serre and Atiyah-Hirzebruch spectral
sequences. We also started a project of doing Homotopy Type Theory in Lean 3, but since the official support for HoTT was dropped from Lean,
this project was not the most convenient way of doing formalization in HoTT.
Related to the formal abstracts project I'm now working on a translation from a controlled natural language to Lean.
I am also interested in mathematical logic. I have worked on type theory, category theory and set theory.
My dissertation was titled On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory and was supervised by my dissertation committee: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz and Mike Shulman.
- Jesse Michael Han, Floris van Doorn. A formalization of forcing and the unprovability of the continuum hypothesis, ITP 2019: Interactive Theorem Proving. (arXiv, Website, Formalization (Github))
- Ulrik Buchholtz, Floris van Doorn, Egbert Rijke. Higher Groups in Homotopy Type Theory, Logic in Computer Science (LICS) 2018. (arXiv, slides, Formalization (Github))
- Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz. Homotopy
Type Theory in Lean, 8th International Conference on Interactive Theorem Proving (ITP),
2017. (arXiv, slides,
(Github), Spectral repository (Github))
- Floris van Doorn. Constructing the Propositional Truncation
using Non-recursive HITs, Certified Proofs and Programs (CPP),
2016. (arXiv, slides,
Lean source (Github))
- Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von
Raumer. The Lean Theorem Prover (system
description), International Conference on Automated Deduction (CADE-25), 2015.
- Cody Roux and Floris van Doorn. The Structural Theory of
Pure Type Systems, Types and Lambda Calculi and Applications (TLCA),
- Floris van Doorn, Herman Geuvers, Freek Wiedijk, Explicit
Convertibility Proofs in Pure Type Systems, Logical Frameworks and Meta-Languages: Theory
and Practice (LFMTP), 2013. (slides, Coq
Talks corresponding to one of my papers are listed under Publications.
- A Formal Abstract of the Classication of Finite Simple Groups, June 2019. Vietnam -- USA Joint Mathematical meeting 2019. slides
- Formal Abstracts, August 2018. Types, Dagstuhl seminar: Formalization of Mathematics in Type Theory. slides.
- Spectral Sequences in Homotopy Type Theory, June 2018. Workshop: Types, Homotopy Type theory, and Verification, Hausdorff Research Institute for Mathematics, Bonn. slides.
- Formalized Spectral Sequences in Homotopy Type Theory, September 2017. Algebra, Combinatorics,
and Geometry seminar, University of Pittsburgh. slides talk 1, slides talk 2.
- Homotopy Type Theory in Lean, July 2017. Computer-aided mathematical proof,
Cambridge. (aimed to people familiar with formalization, but not necessarily
HoTT) slides video.
- The Lean HoTT library, July 2017. Big Proof,
Cambridge. (aimed to people familiar with HoTT) slides video.
- Eilenberg-MacLane spaces in Homotopy Type Theory, March 2017, ASL 2017 North American meeting. slides.
- Homotopy Type Theory in Lean, June 2016, HoTT/UF Workshop colocated with FSCD. slides.
- Reducing higher inductive types to quotients, May
2016, HoTT Workshop in
Toronto. slides, video.
- The Lean Theorem Prover and Homotopy Type Theory (with Jeremy Avigad), May
2016, HoTT Workshop in
Toronto. slides, video.
- Spring 2019: Main instructor for Calculus I (Math 0220).