copilot demo video

Stream: lean4

[Chris Lovett]

Github copilot on Lean4 is sometimes helpful as you can see in this video.
https://www.youtube.com/watch?v=DXvA1qaQFtY

[Jason Rute]

Also, besides copilot itself, there have been a lot of recent papers showing that Codex, the model behind copilot, is pretty good at a lot of Lean- and Isabelle-related tasks like formalizing informal statements, formalizing informal proofs (including ones created by another AI model), informalizing formal Lean code, etc. A lot of it is discussed on #Machine Learning for Theorem Proving . And unlike a lot of research, this work is directly implementable. It is already making its way into VS code plugins for Lean, and into the Lean docs.

[Juan Pablo Romero]

I hope one day features like "generate all cases in a match expression" will get added to VSCode directly, but in the meantime copilot helps:
image.png

[Jason Rute]

I think in Lean 3, you can do that with the {! !} hole syntax.

[Jason Rute]

https://leanprover-community.github.io/mathlib_docs/hole_commands.html#Match%20Stub

[Patrick Massot]

You don't even need this, writing a _ is enough to trigger the code action.