Waterproof: transforming a proof assistant into an educational tool
By Jim Portegies
Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence
By Cyril Cohen
Modularity of special cycles in orthogonal and unitary Shimura varieties
By Salim Tayou