platformer on proof of square root of 3

Stream: general

[Kevin Buzzard]

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]

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]

I have some video

[Sebastian Ullrich]

Haha, sounds awesome

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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