Floris van Doorn

Floris van Doorn

e-mail: fpvdoorn@gmail.com
office: 1.035

I am a professor at the mathematical institute of the university of Bonn since October 2023. I am working on formalized mathematics in the Lean Theorem Prover. I am a maintainer of its mathematical library mathlib, and my latest project was the sphere eversion project. In this project, we formalized an important result in differential topology, namely Gromov’s h-principle for first-order differential relations using a technique called convex integration.

To try Lean, I recommend the online book Mathematics in Lean. Or check out these other ways of learning Lean.

Until September 2023, I was a postdoc at the mathematics department of the University of Paris-Saclay, working with Patrick Massot. Before that, I was a postdoc at the mathematics department of the University of Pittsburgh, working with Tom Hales on the Formal Abstracts and Flypitch projects. I did my PhD at Carnegie Mellon University under the supervision of Jeremy Avigad and Steve Awodey. My dissertation is titled “On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory”. Full CV (pdf).

Research

I formalize mathematical results and develop new tools for the Lean Theorem prover. I am a contributor and maintainer of mathlib. I have formalized results from many areas of mathematics, including measure theory, set theory, model theory, and combinatorics. Together with Jesse Michael Han, I formalized the independence of the continuum hypothesis in the Flypitch project, which was one of the few remaining unformalized problems on Freek Wiedijk’s list. The proof required formalizing an internal model of set theory in Lean and formalizing a notion of forcing. We used Boolean-valued forcing for our proof.

I also formalized another problem on Wiedijk’s list, proving that it is impossible to partition a cube into finitely many smaller cubes. Recently, I have formalized quite some measure theory, including the Haar measure and Fubini’s theorem for the Bochner integral. I have furthermore worked on various tactics, tools, and programs to aid formalization in Lean.

I am interested in Homotopy Type Theory (HoTT), which is a connection between homotopy theory and type theory, where one interprets the basic concepts in the logic of type theory in a geometric way. Using this interpretation, you can define many concepts of algebraic topology, like homotopy and (co)homology groups synthetically into the type theory. 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 have formalized a lot of Homotopy Type Theory in the HoTT library for Lean 2 and in the Spectral Sequence project, where I was the main author of both. My main interest 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 definition of the (cohomological) Serre and Atiyah-Hirzebruch Spectral sequences in Lean.

I have also studied the research question of which higher inductive types can be constructed from ordinary inductive types and one simple higher inductive type, the homotopy pushout.

Publications

Selected Talks

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

Unpublished Work

Past Teaching

University of Pittsburgh

Carnegie Mellon University

Utrecht University