I tried learning Coq through the Software Foundations track a couple times and enjoyed what I did learn, but bounced off. If Coq made something similar to the Natural Number Game [0] I'd love to give it a go and see the differences!

[0] https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...