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:
“Then the justice,
In fair round belly with good capon lined,
With eyes severe and beard of formal cut,
Full of wise saws and modern instances;
And so he plays his part.”
—William Shakespeare (1564–1616)
“It comes to pass oft that a terrible oath, with a swaggering accent sharply twanged off, gives manhood more approbation than ever proof itself would have earned him.”
—William Shakespeare (1564–1616)