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 http://us.metamath

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 http://us.metamath.org/index.html Here is the book which can help with understanding. http://us.metamath.org/downloads/metamath.pdf 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=PL1jSu6GGefBm7RBP0Id2Sa9uyVuyhioAC https://www.youtube.com/playlist?list=PL1jSu6GGefBm7RBP0Id2S... it can be found here, http://us.metamath.org/#mmj2 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 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 https://groups.google.com/forum/#!forum/metamath