Comment by c0balt

The goal (ATP) is similar but the idea is a bit different, sledgehammer is not directly learning/applying rules but instead effectively a driver for invoking a bunch of ATPs + SMT solvers at once on a goal in Isabelle/HOL.

You can read more about it here: https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf