> Finding proofs is the really hard part (NP-hard), and the part which most stands to benefit from "AI" techniques – checking their validity is a lot easier (po

> Finding proofs is the really hard part (NP-hard), and the part which most stands to benefit from "AI" techniques – checking their validity is a lot easier (polynomial time). Note that this is true only for boolean logic and equivalents. Anything stronger has either much higher complexity or is simply undecidable (but proof checking is fast, which is the main point).