Secondary Sylow Theorems. - Jakob von Raumer (Arch. Formal Proofs, 2014)

The Jordan-Hölder Theorem. - Jakob von Raumer (Arch. Formal Proofs, 2014)

The Lean Theorem Prover (System Description). - Leonardo Mendonça de Moura; Soonho Kong; Jeremy Avigad; Floris van Doorn; Jakob von Raumer (CADE, 2015)

Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover. - Jakob von Raumer (ICMS, 2016)

Homotopy Type Theory in Lean. - Floris van Doorn; Jakob von Raumer; Ulrik Buchholtz (ITP, 2017)

Path Spaces of Higher Inductive Types in Homotopy Type Theory. - Nicolai Kraus; Jakob von Raumer (LICS, 2019)

A Syntax for Mutual Inductive Families. - Ambrus Kaposi; Jakob von Raumer (FSCD, 2020)

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. - Nicolai Kraus; Jakob von Raumer (LICS, 2020)

Coherence via Wellfoundedness. - Nicolai Kraus; Jakob von Raumer (CoRR, 2020)

Higher inductive types, inductive families, and inductive-inductive types. - Jakob von Raumer (2020)

A rewriting coherence theorem with applications in homotopy type theory. - Nicolai Kraus; Jakob von Raumer (Math. Struct. Comput. Sci., 2022)