Another famous theorem which is being formalized with a proof assistant is the Kepler Conjecture. It's less than half the size of the ABC Conjecture, with 250 p

Another famous theorem which is being formalized with a proof assistant is the Kepler Conjecture. It's less than half the size of the ABC Conjecture, with 250 pages of much more elementary mathematics, but the leader estimates it will take 20 years to complete. http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proof http://en.wikipedia.org/wiki/Kepler_conjecture#A_formal_proo...