Oak

Suppose you have a potential proof of X and you want to be sure that your proof is correct. X might be a statement of mathematics, philosophy, theology, etc. You just have to write your proof in the language of Oak, and then Oak will tell you whether or not it is correct.

I began work on a proof checker in 2006, and worked on it intermittently over the years. Finally in 2017 I did an initial release, and the project now has its own website and is available on GitHub.

http://oakproof.org