|
|
|
|
|
|
by yesenadam
1514 days ago
|
|
|
From that link: "The first formal proof of the Jordan curve theorem was created by Hales 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." |
|
|