Zulip Chat Archive

Stream: general

Topic: platformer on proof of square root of 3


Kevin Buzzard (Mar 10 2018 at 22:40):

When I was learning about set_option pp.all true a while back, I had recently proved that there was no rational number whose square was 3 in Lean, in no doubt an extremely inefficient manner. I wrote the proof term to a file and I just ran into it again yesterday.

Kevin Buzzard (Mar 10 2018 at 22:41):

I emailed it to my 15 year old son and he imported it into Blender, thickened up the characters, and then ran a platformer game on top of it, with a character with a really bad jump and quite a good grapple trying to get from one end of the proof to the other

Kevin Buzzard (Mar 10 2018 at 22:47):

I have some video

Sebastian Ullrich (Mar 10 2018 at 23:00):

Haha, sounds awesome

Kevin Buzzard (Mar 10 2018 at 23:12):

I'm just taking the sound off it. The hitbox of the character is really small. Sometimes my son just takes gravity off and randomly moves around the proof.

Sebastian Ullrich (Mar 10 2018 at 23:19):

If he ever gets bored, he should play Celeste next :)

Kevin Buzzard (Mar 10 2018 at 23:32):

oh I am such an idiot I switched the video off when he landed on the proof. He grappled around for a while after that. You just see the bit where he falls through the letters a lot here

Kevin Buzzard (Mar 10 2018 at 23:33):

http://wwwf.imperial.ac.uk/~buzzard/sqrt3_fail.mp4

Kevin Buzzard (Mar 10 2018 at 23:40):

oh the grapple will have to wait, it's bed time


Last updated: Dec 20 2023 at 11:08 UTC