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
18
78
20
1,077
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.

Jul 11, 2023 · 2:27 PM UTC

18
15
1
582
Replying to @AlexKontorovich
U think AI can make seminal breakthroughs in Maths?maybe solve millenium problems?
1
1
No
16
Replying to @AlexKontorovich
If ML models can only output based on some combination of their input, does that suggest the proof was similar to previous proofs? If so, does that suggest the proof doesn’t require a brilliant mind, freeing you up for more creative thoughts, while it does the grunt work?
1
8
that's exactly the idea...
10
Replying to @AlexKontorovich
Was the statement itself completely unexpected or was it more a trivial corollary?
1
2
Trivial corollary that would've been annoying to write down, maybe 20 mins worth of work. Done in 2 secs.
4
Replying to @AlexKontorovich
Did it take your conversation into account? I've found that copying and pasting unedited live transcripts into ChaGPT or GPT-4 via the OpenAI Playground yields some similarly incredible results. Even more impressive if it made the suggestion simply based on prior code.
1
2
It had better be just based on previous code! Unless it found a way to hack into my mic...
1
Replying to @AlexKontorovich
Wow. Are you using copilot with lean, or for writing latex?
1
1
Lean. (And LaTeX. And now, general writing.)
Load more