From what I have heard when talking to the people behind formal analysis of protocol security, the main problem currently with using LLMs to 'interact with the theorem prover for you' is that there is nowhere near enough proofs out there for the LLMs to learn how to generalize from them.