Zulip Chat Archive

Stream: lean4

Topic: copilot demo video


Chris Lovett (Oct 12 2022 at 00:31):

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

Jason Rute (Oct 12 2022 at 11:12):

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 (Oct 12 2022 at 16:43):

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 (Oct 12 2022 at 18:57):

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

Jason Rute (Oct 12 2022 at 18:58):

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

Patrick Massot (Oct 12 2022 at 19:03):

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


Last updated: Dec 20 2023 at 11:08 UTC