When I asked experts on formal proofs a year ago, their intuition was that there isn't enough formal proofs out there for LLMs to be very good at the syntax.
It's, as far as I know, quite hard to teach an LLM things it doesn't know.
It's, as far as I know, quite hard to teach an LLM things it doesn't know.
It's a bit frustrating because, before Copilot, new users would come with proofs and you could spend some time helping them write better proofs and they'd learn things and gain skills, but now it's not clear that this is time well spent on my part. Copilot is not going to learn from my feedback.