It looks like we have recently accumulated two more Bachelor thesis-level tasks:
-
Write implementation and proofs for some classic purely functional data structure like queues in several proof assistants (in particular, for cubical type theory based ones and Coq with HoTT) and do detailed comparison of solutions, as outlined here.
-
Prove the Hilbert basis theorem in Coq (possibly several times using different libraries), according to the challenge outlined here.