Floris van Doorn

Floris van Doorn

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

News

Team

Teaching

See also Past Teaching below.

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:

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

See also my full CV (pdf).

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