> check them for truth This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula i

> check them for truth This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula is decidable. That said, LEAN does leverage a SAT solver to try and do a bit of what you describe.