Comment by thwayunion

The wiki article on automated theorem proving is quite bad as an overview of the active field; it's more a historical article about the mid to late 20th century. Most of the interesting things in automated reasoning have happened since the naughts, and that article kind of stops in the 90s

SMT solvers have gotten quite good over the past couple decades, there are tons of domain-specific tools (eg in software and hardware verification), tons of niche applied decidable or semi-decidable theories (eg various modal and description logics), a lot of progress on the proof assistant ("non-fully-automated theorem proving") paradigm, and so on.