I'd like to claim credit for the email, unless someone else contacted him before Monday? Haven't gotten a response myself.

@kenakofer I have confirmed that 13 squares in a square is now listed as proved.

Base rate is really low. Every proved optimal packing on the list was proved in either 1979, 1999, or 2002.

@tom For a larger sample size, you can check out other shape combinations here: https://erich-friedman.github.io/packing/

Even there the most recent update is from 2019

It’s possible there will be renewed interest in these packings in particular, because they have been trending on Twitter lately. I agree it seems unlikely though.

Maybe someone here will see this as a bounty if it gets bid down far enough?

13 might be the easiest.

@JimHays 13 has, purportedly, already been proven and published in the Electronic Journal of Combinatorics (the same place which published Erich Friedman's survey.)

@Nadja_L Since it’s already proved, that points out a bit of disagreement between the question and description. I will side with the more concrete market description here, so if before 2024 the website is updated to show 13 is proved, I will resolve YES, even though it’s not “currently unproved”.

Sounds like free mana for anyone who can convince Erich to update the site based on this paper.