Yesterday I was working on a formalization of something in VS code with GitHub copilot on, talking with a collaborator while sharing my screen over zoom. We finished a theorem, and started discussing what the next natural theorem is. Copilot suggested the complete statement and

Jul 11, 2023 · 2:27 PM UTC

18
78
20
1,076
2/ its proof. I didn't press any keys. We were just talking. As we work, copilot is constantly suggesting things (sometimes good, sometimes not). In this case, it anticipated the complete, correct statement and complete proof. I just hit enter and it was done. Insane.
18
15
1
582
Replying to @AlexKontorovich
If you accept dumb questions on Twitter - what language do you use that vs code and copilot can do proofs in?
3
7
Lean (3 or 4), LaTeX
3
Replying to @AlexKontorovich
You write papers in vscode???
1
2
Replying to @AlexKontorovich
This is really interesting! I see myself doing this when I'm trying to solve a problem. Once you have key ideas/insights in place, connecting them is trivial and could be automated. Would love to see the exact details!
5
Replying to @AlexKontorovich @paulg
I too am seeing it be surprisingly helpful, and understanding of my code and variables. I personally haven’t seen very encouraging results from ChatGPT, even though I keep trying it, but Copilot is definitely worth the $10/mo, just for the fun of it.
1
1
3
Replying to @AlexKontorovich
I can’t decide if that’s a good thing.
16
Replying to @AlexKontorovich
What language were you coding in? Or were you using VS Code as a Latex editor?
Replying to @AlexKontorovich
Was the theorem 1+1=2?
2
1
11
Replying to @AlexKontorovich
I saw co pilot is use and it was awesome I have it but it ain't free 😁
Load more