The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 8/21/21 7:18 PM, Talia Ringer wrote:
> Language models do really well with enough context, and this is often 
> neglected when people try them out, so they often abandon them early. 
> I recently tried Copilot with Joe Cutler in the middle of CompCert to 
> see what it does, and I think even a naive large language model like 
> Codex with no semantic understanding at all does really well at 
> synthesizing proofs inside of a large project specifically when you 
> are in a repetitive file with many similar, small lemmas and slight 
> variations between them. The syntax often captures many of those 
> variations, and the LLM picks up on them easily. We will post a 
> YouTube video on this Monday.
That sounds really interesting, though I'm wondering about the 
comparison point of an Ltac script written by someone very familiar with 
the code base, which would be used for all lemmas.  That's kind of a way 
of making a "style" first-class.