A Formal Proof
In January 2003, Hales announced the start of a collaborative project to produce a complete formal proof of the Kepler conjecture. The aim is to remove any remaining uncertainty about the validity of the proof by creating a formal proof that can be verified by automated proof checking software such as HOL. This project is called Project FlysPecK – the F, P and K standing for Formal Proof of Kepler. Hales estimates that producing a complete formal proof will take around 20 years of work.
Read more about this topic: Kepler Conjecture
Famous quotes containing the words formal and/or proof:
“The formal Washington dinner party has all the spontaneity of a Japanese imperial funeral.”
—Simon Hoggart (b. 1946)
“a meek humble Man of modest sense,
Who preaching peace does practice continence;
Whose pious life’s a proof he does believe,
Mysterious truths, which no Man can conceive.”
—John Wilmot, 2d Earl Of Rochester (1647–1680)