Zulip Chat Archive

Stream: general

Topic: platformer on proof of square root of 3


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

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

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 22:47):

I have some video

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 23:00):

Haha, sounds awesome

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

view this post on Zulip Sebastian Ullrich (Mar 10 2018 at 23:19):

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

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

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 23:33):

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

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 23:40):

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


Last updated: May 10 2021 at 18:22 UTC