I've been running a Lean seminar at CWI/UvA for some time. We now started formalizing Appleby's result on the structure of the single-qudit Clifford group. Here's the blueprint and GitHub repository in case you're interested.
marozols.github.io/clifford-pro...
github.com/marozols/cli...
Lean formalization of the structure theorem for the single-qudit Clifford group - marozols/clifford-project