Shortest Proofs

Stream: new members

[Anand Dyavanapalli]

I'm currently working through the natural number game and it got me wondering:
Is there any place showcasing the shortest proofs for a given problem?

[Kevin Buzzard]

The only level I've been keeping track of the shortest proofs of is the (a+b)^2 level, with the requirement that you're only allowed to use rewrites (so it's not even the shortest proof). I wouldn't really know where to store these shortest proofs. I like my "model solutions" in the github repo -- but I guess I could make another directory for golfed proofs (e.g. cc does most of the levels in Proposition world AFAIR).

[Anand Dyavanapalli]

I'm interested in the shortest proof for $(a + b)^2 = a^2 + b^2 + 2 a b$

[Anand Dyavanapalli]

Where can I find it?

[Anand Dyavanapalli]

I wonder if it's possible to build that directly into the web game i.e. once someone makes a submission, check it against the current shortest proof(s) you have, and revise the list.

[Kevin Buzzard]

I personally couldn't do that, maybe @Mohammad Pedramfar could say something? I only do the lean stuff

[Kevin Buzzard]

show(1:mynat)*_*_=(1:mynat)*_*_+(1:mynat)*_*_ + _,ring

is the shortest that a few minutes of fiddling could get me

[Carl Friedrich Bolz-Tereick]

That's amazing

[Kenny Lau]

@Kevin Buzzard maybe you can ascribe the outermost layer instead?

[Kenny Lau]

Lean elaborates from outside to inside

[Mohammad Pedramfar]

Anand Dyavanapalli said:

I wonder if it's possible to build that directly into the web game i.e. once someone makes a submission, check it against the current shortest proof(s) you have, and revise the list.

It's possible to add an option to the game to show the original proof, the proof written by the people who made the game.
But having the shortest proof written so far would be tricky. This game doesn't store anything on the server side. (The only exception being some statistical data collected by google such as the number of people who visited the page etc) Everything happens in the browser. It doesn't send any data to any server after a level is finished, even the progress is saved inside the browser itself. Having a record of the shortest proof ever written into the game would need some big changes.