Copilot for Lean

Stream: general

[Jason Rute]

Does anyone here use copilot for coding in Lean? If so what does it help with? Is it just good for boilerplate, or is it helpful for writing proofs? Also, would you be willing to send me a (zoomed in) screen shot of it in action that I could use in a talk this week?

[Bulhwi Cha]

I used it last summer. It was hit-or-miss; fun but not very helpful.

[Alex J. Best]

I use it, it's quite often fairly random but occasionally really helpful. I think there was a thread with examples sometimes before. But one of the times I remember being really impressed was when it autocompleted a matrix for me in correct syntax from something like t := ![[1,2,3 sorry on mobile so can't be more precise

[Sorawee Porncharoenwase]

Sorry for resurrecting an old thread, but Copilot really impressed me. It just autocompletes rw [List.mem_join] at h', even though I don't have List.mem_join anywhere in my program.

Does Copilot peek at the proof context window? It would be able to get a lot more localized information that way.

[Wojciech Nawrocki]

@Sorawee Porncharoenwase I don't think it does, which is all the more impressive! For me it has been mostly miss but in some cases, especially with repetitive steps that just differ by a few indices here and there, quite helpful.