The Homotopy Type Theory (HoTT) Game is a project written by a friend and I for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying out mathematics in HoTT. See the website here.