Recent highlights in computer formalized mathematics beyond Lean

The community of mathematicians interacting with computer verified proofs has expanded considerably in recent years alongside the growth of the library Mathlib in the proof assistant Lean4. But in my view, two of the most exciting recent developments in this area require the use of other proof assistants. The first concerns a new proof of the Serre finiteness theorem, stating that the homotopy groups of spheres are finitely presented, by Reid Barton and Tim Campion. It has now been formalized by Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg in Cubical Agda, which implements a cubical variant of homotopy type theory that satisfies canonicity, meaning that the natural numbers involved in the finite presentation can be evaluated to explicit numerals (in theory). The second concerns formalizations of synthetic $\infty$-category theory in the proof assistant Rzk, created by Nikolai Kudasov, and in Agda, in a new library pioneered by Samuel Toth.