The 400-year-old Kepler Conjecture that your local greengrocer knows how to solve

It's something that every greengrocer knows: if you want to stack oranges, the most efficient way is a pyramid with the higher layers of fruit resting in the gaps between the lower layers.

While obvious to fruit stackers, proving it is the best way to fit spheres together has eluded some of the greatest minds in mathematics for more than 400 years.

Proving the best way to fit spheres together has eluded some of the greatest minds in maths for hundreds of years.Credit: iStock

The problem is known as the Kepler Conjecture after the early 17th-century German mathematician Johannes Kepler, who mentions the idea in his 1611 pamphlet The Six-Cornered Snowflake.

Kepler was pondering crystals and spheres and the way pomegranate seeds are stacked inside the fruit, where "the cause of its shape lies in the plant's 'soul' or life-principle".

The most efficient way to stack spheres is similar to this pile of tangerines.

It is one of the longest-standing unsolved problems in mathematics, lasting longer than Fermat's famous last theorem.

Now an international team of mathematicians led by Professor Thomas Hales at the University of Pittsburgh has published its proof of the conjecture, after struggling since 1998 to have it verified.

The formal proof was published this month by Cambridge University Press in Forum of Mathematics, Pi.

In what is a developing method for mathematical proofs, the final publication required the use of powerful computers and code to do the grunt work of verification.

The problem stemmed from Sir Walter Raleigh wanting to efficiently count cannonballs.

But why bother proving what has been obvious to people for so long?

"If we rely on intuition rather than proof we can be led astray because of hidden assumptions," said Associate Professor Stephan Tillman at the University of Sydney, who is not connected to the proof.

Kepler developed his conjecture contemplating snowflakes and pomegranates.

He said as well as the intellectual satisfaction of proving something, there are potential practical outcomes.

"Maybe you want to use the same principle in a different context," he said. By developing a rigorous proof, the principle is transferable to different problems."

The origins of the conjecture come from a very practical problem. In the late 16th century, English explorer Sir Walter Raleigh turned to his scientific adviser Thomas Harriot. He wanted to know an efficient way to count the number of cannonballs on his ships.

This got Harriot thinking about what is also called the "sphere-packing problem". To this conundrum he drew Kepler's attention, and from there Kepler developed what he thought was a self-evident conjecture.

Mathematicians such as Carl Gauss in 1831, made partial proofs of this problem but it wasn't until 1998 that Professor Hales believed he had a complete proof.

At the time a dozen academic referees pored over the mathematics only to get lost, abandoning their task.

The editor of Forum of Mathematics, Pi, Henry Cohn, said: "The verdict of the referees was that the proof seemed to work, but they just did not have the time or energy to verify everything comprehensively.

"To address this situation and establish certainty, Hales turned to computers, using techniques of formal verification. This paper is the result of their completed work."

Associate Professor Norman Wildberger at the University of NSW said these types of problem are no idle question of abstract thought.

"Computational verification already has industrial applications: Toyota and Airbus use similar methods to check how their computer code works," he said.

If you have a computer control system for a car, checking if it works is a laborious process.

Associate Professor Wildberger said you could test it thousands of times and hopefully not get errors.

"However, a more fundamental way is to look at the logical structure of the code. You break down potentially infinite outcomes into finite problems for a computer to verify.

"That gives you a more solid guarantee of surety."

Associate Professor Wildberger, who was not connected to the Kepler conjecture proof, said such an approach will be important in safety verification for driverless cars and similar technologies.