To add to the hail of links, you might want to inspect the big official MIRI progress report on the problem here.

Also, though i know quite a bit less about this topic than the other people here (correct me if I'm wrong somebody), I'm a little suspicious of this distribution because I don't see any way to approximate the length of the shortest proof. Given an unproven mathematical statement for which you aren't sure whether it is true or false, how could you establish even a rough estimate of how hard it is to prove in the absence of actually trying to prove it?