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.

and there's already GPT-f [0], which is a GPT-based automated theorem prover for the Metamath language, which apparently submitted novel short proofs which were accepted into Metamath's archive.

I would very much like GPT-f for something like SMT, then it could actually make Dafny efficient to check (and probably avoid needing to help it out when it gets stuck!)

0. https://analyticsindiamag.com/what-is-gpt-f/

Someone tell Gödel