Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

Bertrand's postulate. - Julian Biendarra; Manuel Eberl (Arch. Formal Proofs, 2017)

Kruskal's Algorithm for Minimum Spanning Forest. - Maximilian P. L. Haslbeck; Peter Lammich; Julian Biendarra (Arch. Formal Proofs, 2019)