2 ms·

I have tried to use some of these theorem proving systems . Since Coq is pretty popular (which means lots of documentation and examples ) I would try that