Most proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text.

The problem is the training corpus tends towards mediocre code. But with an agentic loop that analyzes the code against those criteria and suggests changes then I think it might be possible. I wouldn't try to get it to generate that right off the bat.

IME, LLMs are completely incapable of reasoning about anything remotely difficult. All you'll get are proofs by assertion, not anything rigid you can trust.

I was thinking the same thing!