I used to work quite extensively with Isabelle and as a developer on Sledgehammer [1]. There are well-known results, most obviously the halting problem, that mean fully-automated logical methods applied to a formalism with any expressive capability, i.e. that can be used to formalize non-trivial problems, simply can never fulfill the role you seem to be suggesting. The proofs that are actually generated in that way are, anyway, horrendous -- in fact, the problem I used to work on was using graph algorithms to try and simplify computer-generated proofs for human comprehension. That's the very reason that all the serious work has previously been on proof /assistants/ and formal validation.

LLMs, especially in /conjunction/ with Lean for formal validation, are really an exciting new frontier in mathematics and it's a mistake to see that as just "unreliable" versus "reliable" symbolic AI etc. The OP Terence Tao has been pushing the edge here since day one and providing, I think, the most unbiased perspective on where things stand today, strengths as much as limitations.

[1] https://isabelle.in.tum.de/website-Isabelle2009-1/sledgehamm...