| 2024 | ITP | Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. | Floris van Doorn, Heather Macbeth |
| 2023 | CPP | Formalising the h-Principle and Sphere Eversion. | Floris van Doorn, Patrick Massot, Oliver Nash |
| 2021 | ITP | Formalized Haar Measure. | Floris van Doorn |
| 2020 | CPP | A formal proof of the independence of the continuum hypothesis. | Jesse Michael Han, Floris van Doorn |
| 2020 | LICS | Sequential Colimits in Homotopy Type Theory. | Kristina Sojakova, Floris van Doorn, Egbert Rijke |
| 2019 | ITP | A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. | Jesse Michael Han, Floris van Doorn |
| 2018 | LICS | Higher Groups in Homotopy Type Theory. | Ulrik Buchholtz, Floris van Doorn, Egbert Rijke |
| 2017 | ITP | Homotopy Type Theory in Lean. | Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz |
| 2016 | CPP | Constructing the propositional truncation using non-recursive HITs. | Floris van Doorn |
| 2015 | CADE | The Lean Theorem Prover (System Description). | Leonardo Mendona de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |