Zulip Chat Archive

Stream: new members

Topic: Shortest Proofs


view this post on Zulip Anand Dyavanapalli (Jul 21 2020 at 17:03):

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?

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 17:39):

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).

view this post on Zulip Anand Dyavanapalli (Jul 21 2020 at 18:02):

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

view this post on Zulip Anand Dyavanapalli (Jul 21 2020 at 18:02):

Where can I find it?

view this post on Zulip Anand Dyavanapalli (Jul 21 2020 at 18:04):

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.

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 18:06):

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

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 18:23):

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

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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 21 2020 at 18:29):

That's amazing

view this post on Zulip Kenny Lau (Jul 21 2020 at 18:32):

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

view this post on Zulip Kenny Lau (Jul 21 2020 at 18:33):

Lean elaborates from outside to inside

view this post on Zulip Mohammad Pedramfar (Jul 24 2020 at 02:46):

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.


Last updated: May 15 2021 at 00:39 UTC