My recollection of calculus disagrees with your initial proposition. When the algorithm pool grows wide enough you have to apply reason to pick the correct strategy.
Yes, try doing beute force theorem proving using something like Idabelle/HOL sledgehammer optimized search. There are cases where it will try brute force essentially forever when asking one or two questions solves the problem.
The system has some heuristics to ask questions and specify things it found incomplete.
GPT is meant to interactively ask those questions. It fails at it.
