Isabelle[1], Coq[2], and Metamath[3] are probably the three most well-known automated proof assistants but there are many others[4]. Using them is very similar

Isabelle[1], Coq[2], and Metamath[3] are probably the three most well-known automated proof assistants but there are many others[4]. Using them is very similar to programming - the mathematician writes his proof in a formal language using a text editor or IDE, and a "compiler" either verifies the proof or produces error messages. Most of these also have features which "assist" the author by automatically searching for formal steps to fill in the gaps between what the author wrote. They also provide libraries/modules/packages for topics like number theory, geometry, calculus, etc., so that you can build off of standard definitions and well-known theorems instead of starting from scratch. Of these, Isabelle and Coq compete for best-of-breed and are extremely powerful. Metamath on the other hand is intentionally minimalist, starting at a level below logic (string substitution rules, basically) and building up predict logic inside the system. Metamath comes with a "proof explorer"[5] - an online body of proofs formally verified by metamath. For proofs about algorithms in particular, TLA+ [6] is a formal specification language which can prove things about algorithms, as charmingly described in "Euclid Writes an Algorithm."[7] [1]: https://isabelle.in.tum.de/ https://isabelle.in.tum.de/ [2]: https://coq.inria.fr/ https://coq.inria.fr/ [3]: http://us.metamath.org/ http://us.metamath.org/ [4]: https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant [5]: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html [6]: https://learntla.com/introduction/ https://learntla.com/introduction/ [7]: https://lamport.azurewebsites.net/pubs/euclid.pdf https://lamport.azurewebsites.net/pubs/euclid.pdf