Zulip Chat Archive

Stream: general

Topic: RSA in Lean

Johan Commelin (Sep 12 2018 at 08:11):

I have to give a talk for high school students. Topic: cryptography.
I've done this before, and I would usually fool around in Python. Does anyone know of an implementation of DH or RSA in Lean?

Mario Carneiro (Sep 12 2018 at 08:12):

lolno

Kevin Buzzard (Sep 12 2018 at 08:12):

I stay away from Lean when I'm giving talks like this. I spend time talking about WhatsApp because that's what they know in the UK.

Johan Commelin (Sep 12 2018 at 08:12):

But you could do both, right?

Mario Carneiro (Sep 12 2018 at 08:12):

then again, all you need is a bit of group exponentiation on zmod to implement DH

Kevin Buzzard (Sep 12 2018 at 08:13):

My school talks are usually only 30-40 mins

Mario Carneiro (Sep 12 2018 at 08:13):

and I think RSA is about as easy

Johan Commelin (Sep 12 2018 at 08:13):

Aah, I have 75 minutes. The students are coming to an open day of the math department.

Kevin Buzzard (Sep 12 2018 at 08:13):

I might even be tempted to refuse to speak to schoolkids for so long. They're not used to concentrating for that kind of time (at least in the UK)

Kevin Buzzard (Sep 12 2018 at 08:14):

I would talk for 30, give them 15 minutes to do a project, and then talk for 30 more. Active learning!

Johan Commelin (Sep 12 2018 at 08:14):

You've got tenure :lol: Refusing is not on my list of options.

Johan Commelin (Sep 12 2018 at 08:14):

Right, that's what I was thinking.

Kevin Buzzard (Sep 12 2018 at 08:14):

They could spend the 15 minutes trying to install Lean :-)

Johan Commelin (Sep 12 2018 at 08:14):

So they could do their project with a hand calculator or python or whatever.

Johan Commelin (Sep 12 2018 at 08:14):

I was just thinking of demoing Lean. Not them playing with it.

Kenny Lau (Sep 12 2018 at 08:15):

oh no it takes a whole hour to install lean

Kevin Buzzard (Sep 12 2018 at 08:15):

maybe a 7 minute talk, then an hour working together trying to install Lean, and then 8 minute wrap-up at the end.

Kevin Buzzard (Sep 12 2018 at 08:16):

I've done super-hard computations on my phone using the pari-gp app and a bluetooth keyboard.

Kevin Buzzard (Sep 12 2018 at 08:16):

and the app is a one click install on Android.

Kevin Buzzard (Sep 12 2018 at 08:16):

You could give them some 5 digit numbers to factor on their stock calculator

Kevin Buzzard (Sep 12 2018 at 08:17):

but I would stay away from Lean. I've tried it with Math Olympiad level schoolkids and they found it tough

Johan Commelin (Sep 12 2018 at 08:17):

Ok, thanks for the advice. I'll stick to python.

Kevin Buzzard (Sep 12 2018 at 08:18):

on the other hand I should say that on some Wed in mid-Oct (18th?) I am giving another Lean school talk.

Kenny Lau (Sep 12 2018 at 08:18):

can I come? :P

Mario Carneiro (Sep 12 2018 at 08:19):

If you are interested in incorporating lean, you can just mention it without going in depth. Make them know formal proving is a thing, and move on

Johan Commelin (Sep 12 2018 at 08:21):

Right. That's also an option.

Kevin Buzzard (Sep 12 2018 at 08:37):

can I come? :P

My recent experience with going to give school talks in the UK is that you can't get beyond the entrance until you've proved (or at least claimed) that you're the person they're expecting to give the talk, and they've given you something to wear around your neck saying "visitor".

Kevin Buzzard (Sep 12 2018 at 08:37):

It's very different to how it was 20 years ago

Kevin Buzzard (Sep 12 2018 at 08:37):

so my guess is no

Last updated: Dec 20 2023 at 11:08 UTC