Isabelle is a generic proof assistant. It provides infrastructure for formally expressing mathematical formulas and proving those formulas correct.
The most widely used Isabelle-based system is Isabelle/HOL, which provides an environment for proving higher-order logic theorems.
Sledgehammer interfaces Isabelle/HOL with first-order logic resolution provers, of which there are many, as well as SMT solvers (paper). It has an approach to relevance filtering that seems surprisingly effective for its crudeness - basically prioritizing simplification rules by number of shared symbols.
The jEdit IDE is probably the friendliest way to kick Isabelle's tires (not saying much).
Isabelle/HOL manual, Programming and Proving in Isabelle/HOL
Isabelle/Isar manual
INFR09042 at University of Edinburgh
CS 576 at University of Illinois
FOMUS 2016 workshop
Some miscellaneous examples