In case you need a break from some of the gloom and doom in the news today, TheBlaze has a very interesting story about a 400-year-old math problem that has finally been solved. Have you ever been in a grocery store and wondered what the most efficient way to stack round objects is? Well, now we have a definitive answer.

“A critical 400-year-old -math problem has finally been solved,” Pat joked on radio this morning. “Maybe.”

Way back in 1611, Johannes Kepler hypothesized a pyramid arrangement would be the best way to stack a collection of round objects. While the concept quickly became common practice, Kepler was never able to mathematically prove his theory.

Four centuries later, we now have proof.

According to New Scientist, a computer program that was more than a decade in the making has proven Kepler’s theory with 100% certainty. University of Pittsburgh mathematician Thomas Hales is the man who corroborated the claims.

But even Hale struggled through some 15 years of searching before he could prove the answer to this long unproven question. New Scientist reports:

Hales first presented a proof that Kepler's intuition was correct in 1998… But the proof was a 300-page monster that took 12 reviewers four years to check for errors. Even when it was published in the journal Annals of Mathematics in 2005, the reviewers could say only that they were "99 per cent certain" the proof was correct.

So in 2003, Hales started the Flyspeck project, an effort to vindicate his proof through formal verification. His team used two formal proof software assistants called Isabelle and HOL Light, both of which are built on a small kernel of logic that has been intensely scrutinised for any errors – this provides a foundation which ensures the computer can check any series of logical statements to confirm they are true.

On Sunday, the Flyspeck team announced they had finally translated the dense mathematics of Hale's proof into computerised form, and verified that it is indeed correct.

“So really, honestly, it was the pile versus the pyramid and they couldn't figure out why,” Glenn asked on radio this morning. “They know [for certain] about global warming… [but it] took 400 years to figure out how to stack oranges?”