U.S. scientists deliver formal proof of famous Kepler Conjecture

Updated 2017-06-20 10:09:48 Xinhua

An international team of mathematicians led by University of Pittsburgh mathematician Thomas Hales has delivered a formal proof of the Kepler conjecture, a famous problem in discrete geometry that had gone unsolved for more than 300 years.

The team's paper is recently published in the journal Forum of Mathematics, Pi, an open access journal published by Cambridge University Press.

The Kepler Conjecture was a famous problem in discrete geometry, which asked for the most efficient way to cram spheres into a given space.

The answer, while not difficult to guess, had been remarkably difficult to prove. Johannes Kepler, the famous mathematician and astronomer predicted this 300 years ago, but he couldn't prove it.

No one proved it for 300 years. In 1998, professor Hales and his student Sam Ferguson originally announced a proof. But the solution was so long and complicated that a team of a dozen referees spent years working on checking it before giving up.

"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," Henry Cohn, editor of Forum of Mathematics, Pi, said in a statement.

"The proof was published in 2005, and no irreparable flaws were ever identified, but it was an unsatisfactory situation that the proof was seemingly beyond the ability of the mathematics community to check thoroughly," said Cohn, also a principal researcher at Microsoft Research New England in Cambridge, Massachusetts.

"To address this situation and establish certainty, Hales turned to computers, using techniques of formal verification. He and a team of collaborators wrote out the entire proof in extraordinary detail using strict formal logic, which a computer program then checked with perfect rigor. This paper is the result of their completed work," Cohn said.

This paper not only settles a centuries-old mathematical problem, but is also a major advance in computer verification of complex mathematical proofs, Cambridge University Press, the oldest university press and one of the oldest publishers and printers in the world, said in a press release.

Also in the News

Nicole Kidman Recalls Oscar Glory: Loneliest Time
Showbiz2016/06/16 13:58December 10 2018 23:34:04

Nicole Kidman Recalls Oscar Glory: Loneliest Time

Attending Shanghai International Film Festival, Nicole Kidman talks about her role in "Grace of Monaco".

Labor Day Travel Peak Starts
Also in the News2014/05/01 12:16December 10 2018 23:34:04

Labor Day Travel Peak Starts

Johnny Depp Delivers a Speech 'Evolve the Future' in 'Transcendence'
Also in the News2014/04/18 13:18December 10 2018 23:34:04

Johnny Depp Delivers a Speech 'Evolve the Future' in 'Transcendence'

Hollywood star Johnny Depp's speech in the upcoming new film "Transcendence" has been disclosed on Friday, April 11th.

China World Business Sports Showbiz Audio
C4 My Chinese Life The Sound Stage China Revealed Showbiz Video Travel Video
China World Fun Travel Entertainment Sports
Beijing Shanghai Guangzhou
Live Music Opera & Classical Movies Traditional Shows Exhibitions
Learn Chinese:
Chinese Studio Living Chinese Everyday Chinese Just For Fun Chinese Culture Buzzwords