Johan Commelin, Robert Y. Lewis: Formalizing the ring of Witt vectors. CPP 2021: 264-277