For k >= 1, the central entry of a perfect magic hypercube of order 2k+1 and dimension k+1 is the average of all its entries.

This is the centre value question in Christian Boyer's Problem 10. The Lean proof is on GitHub.