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.
