The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> I think it's worth noting that OpenAI (the company that made Codex, the
> model behind Copilot) has an ongoing project on neural proof synthesis for
> Lean.  I think we will see some use of this in the near future.  For that
> week, I'm likely to invite someone at OpenAI to give a talk and demo the
> model if he's allowed. (Coq will get left behind from that effort, by the
> way, if nobody adds Coq proofs for their cross-language benchmarks; if
> interested in that effort, let me know.)

FWIW, as a professor, I'd feel ... awkward inviting presentations about
tools that include a sufficiently large amount of secret/proprietary
elements that one can't just go and reproduce it on your own.
It seems philosophically opposed to ideas such as "open access".


        Stefan