CoqPilot

Stream: Machine Learning for Theorem Proving

[Jason Rute]

JetBrains (the makers of the IntelliJ and PyCharm IDEs as well as the Arend interactive theorem prover), made a recent Coq VSCode plugin called CoqPilot which integrats the coq-lsp server with OpenAI's LLMs to do proof completion. I have no idea if it is any good. It might be more of a proof of concept of the user interface. There is a discussion on the Coq Zulip.