This repo contains a reimplementation of the Lean Mathlib tauto tactic, i.e. a tactic to prove tautologies in propositional logic.

This project is just a learning exercise -- the implementation is 200 lines long and completely naive, and one should expect it to be dramatically slower than an implementation of a standard SAT algorithm like DPLL. Check out duper, by Josh Clune, if you are looking for something performant.