Auto-hyperlinking the Stacks Project. - Johan Commelin; Josef Urban (CICM (Work in Progress), 2015)

Formalising perfectoid spaces. - Kevin Buzzard; Johan Commelin; Patrick Massot (CPP, 2020)

Formalizing the ring of Witt vectors. - Johan Commelin; Robert Y. Lewis (CPP, 2021)

Abstraction boundaries and spec driven development in pure mathematics. - Johan Commelin; Adam Topaz (CoRR, 2023)

Anatomy of a Formal Proof. - Jeremy Avigad; Johan Commelin; Heather Macbeth; Adam Topaz (CoRR, 2024)