Agda

Agda is a proof assistant program that can be used to formalize mathematical proofs. I used it to work through part of the Homotopy Type Theory Book.

https://github.com/shaunharker/AgdaHoTT

https://shaunharker.com/agda