It seems to me that the optimality for regular octagons is not rigorously proven up to now. The cited paper of Atkinson-Jiao-Torquato does not prove the optimality in the case of regular octagons (they do computer simulations which give the best known packing).