Zulip Chat Archive

Stream: general

Topic: RSA in Lean


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 08:12):

lolno

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:12):

But you could do both, right?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 08:12):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:13):

My school talks are usually only 30-40 mins

view this post on Zulip Mario Carneiro (Sep 12 2018 at 08:13):

and I think RSA is about as easy

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:14):

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

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:14):

Right, that's what I was thinking.

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:14):

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

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:14):

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

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:14):

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 08:15):

oh no it takes a whole hour to install lean

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:16):

and the app is a one click install on Android.

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:16):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:17):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 12 2018 at 08:18):

can I come? :P

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 12 2018 at 08:21):

Right. That's also an option.

view this post on Zulip 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".

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:37):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 08:37):

so my guess is no


Last updated: May 17 2021 at 22:15 UTC