The essay ‘On the six-cornered snowflake,’ which was written by the German astronomer Johannes Kepler in 1611, contains the statement of what is now known as the Kepler conjecture: ‘no packing of congruent balls in Euclidean three-space has density greater than that of the face-centered cubic packing.’

This conjecture is the oldest problem in discrete geometry.

The answer to the Kepler conjecture, while not difficult to guess, had been remarkably difficult to prove.

Prof. Hales and his student Sam Ferguson originally announced a proof in 1998, 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,” said Henry Cohn, editor of Forum of Mathematics, Pi, and principal researcher at Microsoft Research New England in Cambridge, Massachusetts.

“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.”

“To address this situation and establish certainty, Prof. Hales turned to computers, using techniques of formal verification,” Cohn explained.

“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.”

The paper not only settles a centuries-old mathematical problem, but is also a major advance in computer verification of complex mathematical proofs.

Source: Sci News