Computer finally proved the answer to "Which is the best way to stack fruits?" That existed 400 years ago

ByJames Yu

"The method of stuffing the spheres most efficiently in the box is the same way that the fruit shop builds up oranges at storefrontsThe accuracy of the proof of the problem presented 400 years ago was finally proved by the computer.

Proof confirmed of 400 - year - old fruit - stacking problem - physics - math - 12 August 2014 - New Scientist
http://www.newscientist.com/article/dn26041-proof-confirmed-of-400yearold-fruitstacking-problem.html

The question "What is the best way to stack spheres?" Is related to planetary motionKepler's lawI recitedJohannes KeplerIn 1611, it was initiated that "The most effective way is to build a pyramid style as the fruit shop builds up oranges", but it has not been certified until now did.

It proved this problem called Kepler's prediction that the University of PittsburghThomas HalesDoctor. Dr. Hales told the impression at that time "I felt suddenly rejuvenated about 10 years old."

ByRachel Patterson

However, according to Dr. Hales, the proof of Kepler's prediction was completed in 1998. There are infinite ways to stack spheres, but most of it is just a variation of thousands of methods. Therefore, Dr. categorized the stacking method into thousands of kinds that can be mathematically expressed, and investigated using software.

However, because the proof was a huge amount spanning 300 pages, 12 reviewers confirmed the right and wrong over 4 years. In 2005 it was "correct with 99% probability"Annals of MathematicsIt was decided to be presented in the magazine.

On the other hand, in 2003 the research team of Dr. Hales et al. Started a project named "FlySpec (small stain)". Although the Kepler prediction was proved with 99% accuracy, the research team further verified that the proof is correct using a program with a kernel that also examines small errors "Isabelle" and "HOL Light" I checked it.

ByStéphane PIA

And on Sunday, 10th August 2014, the FrySpec team announced that the proof was correct as a result of rigorously checking Dr. Hales' certification on the computer.

About this, Dr. Hales says "Humans have no need to evaluate the correctness of mathematical proof by technology." I have not participated in the research, Professor Alan Bandi of the University of Edinburgh also evaluates the research of Freiseck, "This is a big step", and as many a mathematician in the future will aid in the proof I will be using a computer. "A sociological event that a world mathematician has reached out to an automatic theorem prove is a very important element and it will be a future case study."

It is difficult for humans to see everything in a bird's-eye view, so it is very meaningful to be able to check the proof of mathematics by the program. Professor Hales said, "There are lots of ideas I would like to do while the official verification is taking place, hopefully the next project will not take 20 years!"