Checking proofs is decidable. Coming up with proofs is undecidable.

This tool does the former, leaving the latter up to humans.