Agreed! The most famous mathematician in the field told me “I used the first tool I could understand how to write a proof in.” Most he could not! I was so d

Agreed! The most famous mathematician in the field told me “I used the first tool I could understand how to write a proof in.” Most he could not! I was so disgusted by the tutorials for Coq that I wrote my own. It has been reviewed positively on Hacker News before. If you want a look at some of the basics of formal proof and these tools, take a look: http://michaeldnahas.com/doc/nahas_tutorial.html http://michaeldnahas.com/doc/nahas_tutorial.html