If you can program you might like Metamath, it feels quite a lot like writing code.

Here is the main site. http://us.metamath.org/index.html

Here is the book which can help with understanding. http://us.metamath.org/downloads/metamath.pdf

Here are some tutorials for MMJ2 which is the main proof assistant to use, https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2S...

it can be found here, http://us.metamath.org/#mmj2

Here are some beginners proof exercises which are a good place to start out

http://us.metamath.org/mpegif/mmtheorems289.html#mm28844b

I will warn you though it is a bit like the wild west, it is not easy to accomplish anything and it is exciting to be on the frontier.

The community is really cool, you can chat with them here.

https://groups.google.com/forum/#!forum/metamath