Floris van Doorn

e-mail: fpvdoorn@gmail.com
office: Endenicher Allee 62 (the building next to the Math department), room 1.002

News

• October 2024: There is an almost weekly seminar on Friday at 14:15-16:00 in room N0.003 on formalization. See the seminar schedule below.
• October 2024: This semester I’m organizing a weekly Lean hacking session on Wednesdays 18:15-20:00 in seminar room 0.006. Feel free to join. There will be cookies!
• October 2024: Maria, Michael and Arend joined the formalization group in Bonn.
• September 2024: We are halfway done with the Carleson’s project! This is by counting the number of lemmas formalized.
• June 2024: 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.

Team

• María Inés de Frutos-Fernández (postdoc)
• Michael Rothgang (postdoc)
• Arend Mellendijk (PhD student)

Teaching

• WiSe 24/25: Formalized Mathematics in Lean
• SuSe 24: Collaborative Formalization in Analysis
• WiSe 23/24: Formalized Mathematics in Lean

See also Past Teaching below.

Seminar Schedule

Seminar repository

• 18.10 Arend Mellendijk on monadic programming in Lean
• 25.10 Floris van Doorn on metaprogramming in Lean
• 01.11 No seminar
• 08.11 Floris van Doorn on metaprogramming in Lean
• 15.11 TBA
• 22.11 TBA
• 29.11 TBA
• 15.11 TBA
• 06.12 TBA
• 13.12 TBA
• 20.12 TBA
• 10.01 TBA
• 17.01 TBA
• 24.01 TBA
• 31.01 TBA

About me

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.
• I contributed to the formalization of the Polynomial Freiman-Ruzsa Conjecture.
• 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 learn 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. I also enjoy thinking about combinatorial problems, solving puzzles and playing board games and video games.

Short CV

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

Publications

• Floris van Doorn, Heather Macbeth. Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality, ITP 2024: Fifteenth Conference on Interactive Theorem Proving. (slides)
• Patrick Massot, Floris van Doorn, Oliver Nash. “Formalising the *h*-principle and sphere eversion”, CPP 2023: Certified Programs and Proofs. (paper, 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)

Selected Talks

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

• Formalizing a proof of Carleson’s theorem, Oct 2024. Homotopy Type Theory Electronic Seminar Talks, online. (slides, recording)
• 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)

Unpublished Work

• 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

Past Teaching

University of Pittsburgh

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

Carnegie Mellon University

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

Utrecht University

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