## 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: May 10 2021 at 18:22 UTC