Ideas for a talk for undergraduates with various scientif...

Stream: general

[Riccardo Brasca]

Dear all,
I will give an introductory talk about proof assistants to students and I am looking for ideas on what to speak about. The audience will be mainly first/second year undergraduates in mathematics, but also I'm computer science, physics and maybe chemistry.

My plan is to start presenting proof assistants as "labs" where we can do math, like people do physics in labs, and show some simple proofs. I will also surely say something about software verification and AI, maybe be asking live gpt to prove something.

Do you have any suggestions on things to show? It's a rather informal talk so I am free to do whatever I want.

Thanks!

[Kevin Buzzard]

An example talk for that audience: prove that composite of continuous functions is continuous, first with copilot off and a brute force proof, then with some gimmicks like continuity or hg.comp hf and then with copilot on. Then ask them how much further do they think it can get, then show them PFR and eg Bhavik's formalisation this week of November's counterexample to fishbone, then say that this is what humans can do so we're ahead of AI because they can only get a silver medal in the IMO and show them the deep mind blog and you should still have some time left for other stuff

[Riccardo Brasca]

Turning copilot on in the middle of the talk is a good idea!

[Kevin Buzzard]

Yeah, as both Patrick and me discovered recently, turning it on at the beginning after you've rehearsed gives a rather misleading picture :-)

[Jeremy Avigad]

It's disconcerting. Copilot seems to remember not just the last 20 files you opened, including stuff you deleted, but also what you looked at in your browser earlier in the day, what you ate for breakfast, and what you were thinking about when you ate it.

[Kim Morrison]

I find that whenever I commit some work it (Cursor, rather than Copilot) remembers less --- the current git diff is high in its context window.