Floris van Doorn

Floris van Doorn

e-mail: fpvdoorn@gmail.com

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).

Research

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.

Dissertation

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.

Publications

Posts on the HoTT Blog

Other work

Selected Talks

Talks corresponding to one of my papers are listed under Publications.

Teaching

Pitt CMU UU