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 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:

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.


Short CV

See also my full CV (pdf).


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