This is moreso automation-assisted theorem proving. It takes a lot of human work to get a problem to the point where automation can be useful.

It's like saying that calculators can solve complex math problems; it's true in a sense, but it's not not strictly true. We solve the complex math problems using calculators.