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

I am a professor at the mathematical institute of the university of Bonn and leading the workgroup Formal Mathematics. My interest is to make it viable to formalize research mathematics in *proof assistants* that can check the correctness of such proofs for you. Currently, it still takes a lot of work to write the proof down in great details.

I am mainly working using the Lean Theorem Prover, and I am a maintainer of its mathematical library mathlib. Projects that I’ve done include:

- The Carleson project, proving Carleson’s theorem generalized to doubling metric measure spaces.
- The sphere eversion project, formalizing Gromov’s h-principle and concluding the existence of an eversion of a sphere.
- The Flypitch project, formalizing the independence of the continuum hypothesis.
- The Spectral sequences project, formalizing the (cohomological) Serre spectral sequence using synthetic homotopy theory. This was written on top of the HoTT library for Lean 2.

To get a feel for Lean, try out the Natural Number Game or read the online book Mathematics in Lean. There are also other ways of learning Lean.

I am interested in formalized mathematics, tools and automation for formalization and (homotopy) type theory.

*June 24*: I’m launching the formalization of Carleson’s theorem. Take a look at the project webpage, or the introductory presentation. If you know some Lean, you are welcome to join the project.*Summer 24*: I’m teaching a seminar Collaborative Formalization in Analysis (pdf, repository)*Winter 23/24*: I’m taught Formalized Mathematics in Lean

- October 2023 - present: Professor at the University of Bonn
- 2021 - 2023: Postdoc at the mathematics department of the University of Paris-Saclay, working with Patrick Massot.
- 2018 - 2021: Postdoc at the mathematics department of the University of Pittsburgh, working with Tom Hales on the Formal Abstracts and Flypitch projects.
- 2013-2018: 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”*.

See also my full CV (pdf).

- Floris van Doorn, Heather Macbeth.
*Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality*, to appear at ITP 2024. - Patrick Massot, Floris van Doorn, Oliver Nash.
*“Formalising the *h*-principle and sphere eversion”*, CPP 2023: Certified Programs and Proofs. (ACM, arXiv, website, slides) - Jeremy Avigad, Floris van Doorn.
*“Progress on a Perimeter Surveillance Problem”*, ICAS 2021: International Conference on Autonomous Systems. (arXiv, proceedings) - Floris van Doorn.
*“Formalized Haar Measure”*, ITP 2021: Interactive Theorem Proving. (arXiv, Formalization is part of mathlib) - Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis.
*“Maintaining a Library of Formal Mathematics”*, CICM 2020: 13th Conference on Intelligent Computer Mathematics. (arXiv) - Kristina Sojakova, Floris van Doorn, Egbert Rijke.
*“Sequential Colimits in Homotopy Type Theory”*, LICS 2020: Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science. (Formalization (Github)) - The mathlib Community.
*“The Lean Mathematical Library”*, CPP 2020: Certified Programs and Proofs. (arXiv, Website, Formalization (Github)) - Jesse Michael Han, Floris van Doorn.
*“A Formal Proof of the Independence of the Continuum Hypothesis”*, CPP 2020: Certified Programs and Proofs. (arXiv, Website, Formalization (Github)) - 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, Lean-HoTT library (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), 2014. (slides) - 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 formalization)

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

*Towards a formalized proof of Carleson’s theorem*, June 2024. Workshop: Formalization of Mathematics, Bonn (slides, recording, webpage)*Primes, Proofs and Computers*, inaugural lecture, May 2024. (slides, Lean demo)*The Sobolev inequality in Lean*, March 2024. Informal Formalization Seminar, Amsterdam. (slides)*The internals of Lean*, January 2024. Computer-verified proofs: 48 hours in Rome. (slides, workshop repository)*Mathematics in Lean*, Hausdorff School, Bonn, Germany, September 2023. (slides, school repository)*The Independence of the Continuum Hypothesis in Lean*, September 2023. Lean for the Curious Mathematician Colloquium, Düsseldorf, Germany. (slides)*Formalizing sphere eversion using Lean’s mathematical library*, June 2023. Special session on Machine-checked mathematics, CALCO 2023 & MFPS XXXIX, Bloomington, Indiana, USA. (slides)*Tutorial on interactive theorem proving in Lean*, June 2023. Logic Colloquium, Milan. (slides, repository)*What can we learn from formalizations in homotopy type theory?*, May 2023. Formalization of Cohomology Theories, Banff International Research Station. (slides)*Lessons Learned from Formalizing Local Convex Integration*, May 2022. Lean in Lyon. (slides)*Formalizing mathematics in Lean*, November 2021. Laboratoire Méthodes Formelles. (slides)*Automating Concept Equivalence in Dependent Type Theory*, September 2021. 6th Conference on Artificial Intelligence and Theorem Proving (AITP), online. (slides, video starts around 2:19:00).*Structures and Classes*, July 2020. Lean for the curious mathematician, online. (video 1, video 2)*Tactics in Lean*, February 2020. HCM Workshop: Mathematical Language and Practical Type Theory. (slides)*Lean Tactics*, January 2020. Formal Methods in Mathematics / Lean Together, Pittsburgh.*A Formal Abstract of the Classification of Finite Simple Groups*, June 2019. Vietnam — USA Joint Mathematical meeting 2019. (slides)*Towards Spectral Sequences for Homology*, November 2018. Homotopy Type Theory Electronic Seminar Talks, online. (slides, video)*Formal Abstracts*, August 2018. 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. (slides, video)*The Lean HoTT Library*, July 2017. Big Proof, Cambridge. (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*, May 2016 (with Jeremy Avigad), HoTT Workshop in Toronto. (slides, video)*Eilenberg-MacLane Spaces in Homotopy Type Theory*, March 2016, ASL 2017 North American meeting. (slides)

*Carleson Operators on Doubling Metric Measure Spaces*, Lars Becker, Floris van Doorn, Asgar Jamneshan, Rajula Srivastava, Christoph Thiele. Preprint and blueprint for Lean formalization (arXiv, Github)*Designing a general library for convolutions*, Floris van Doorn. Preprint (arXiv)*On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory*, Floris van Doorn. Dissertation. Committee: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, and Mike Shulman.*Logic and Proof*, Jeremy Avigad, Robert Y. Lewis, Floris van Doorn. Lecture notes for the course Logic and Mathematical Inquiry (Interactive version)*The Lean Theorem Prover*, Floris van Doorn. Blog post of the HoTT Blog, December 2015. (Link)*Constructing the Propositional Truncation using Nonrecursive HITs*, Floris van Doorn. Blog post of the HoTT Blog, July 2015. (Link)- Short notes on the
*Applications of the Serre Spectral Sequence*, November 2015. *Propositional Calculus in Coq*, Floris van Doorn. (arXiv:1503.08744), May 2014.*Explicit Convertibility Proofs in Pure Type Systems*, Floris van Doorn. Master thesis. Advisor: Freek Wiedijk

- Spring 2021: Abstract Algebra (Math 1250).
- Spring 2020: Topics in Geometry (Math 1290).
- Spring 2019: Calculus I (Math 0220).

- Fall 2016: TA for Differential and Integral Calculus (21-120) with Russ Walker.
- Fall 2015: TA for Logic and Mathematical Inquiry (80-211) with Jeremy Avigad. Also co-author of the lecture notes together with Jeremy Avigad and Rob Lewis.
- Spring 2015: TA for Game Theory (80-405/80-705) with Adam Bjorndahl.
- Fall 2014: TA for Formal Logic (80-310/80-610) with Steve Awodey.

- Spring 2012: TA for Discrete Mathematics with Han Hoogeveen.
- Fall 2011: TA for Foundations of Mathematics with Jaap van Oosten.