the first formal proof of the jordan curve theorem was created by in the hol light system, in january 2005, and contained about 60,000 lines. another rigorous 6,500-line formal proof was produced in 2005 by an international team of mathematicians using the mizar system. both the mizar and the hol light proof rely on libraries of previously proved theorems, so these two sizes are not comparable. showed that the jordan curve theorem is equivalent in proof-theoretic strength to the weak könig's lemma.