Yes, try doing beute force theorem proving using something like Idabelle/HOL sledgehammer optimized search. There are cases where it will try brute force essent

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.