×

zbMATH — the first resource for mathematics

The Jordan curve theorem, formally and informally. (English) Zbl 1137.03305
From the introduction: Today, there is an ambitious long-term endeavor to translate a large body of mathematics into formal proofs that can be read and checked by computer. Such computer systems check every logical inference of every lemma, theorem, and corollary all the way back to the fundamental axioms of mathematics. Even a simple arithmetic identity such as \(1+1=2\) is checked thoroughly from the basic principles of arithmetic, rather than relying on the arithmetic capabilities of the computer chip. While it is impossible to avoid every potential source of defect in a real-world computer, the designers of these systems continue to make every effort to provide the greatest mathematical rigor attainable by current technology.
One computer system that checks the correctness of mathematical proofs is called MIZAR. The MIZAR group has made the computer verification of the Jordan curve theorem a pet project.
In January 2005, I completed a formal proof of the Jordan curve theorem in a different computer system, called HOL Light. (HOL Light is so named for being a lightweight implementation of Higher-Order-Logic.) The implementation took me months of rather intensive work at a computer. In September 2005, the MIZAR team completed their formal proof of the same theorem. The formal proof of the Jordan curve theorem in HOL Light consists of 138 definitions, 1381 lemmas, and over 44,000 proof steps spread over 59,000 lines of computer code. There are approximately 20 million primitive logical inferences in this proof of the Jordan curve theorem.
A formal proof typically begins with a careful conventional proof. Each lemma is then expanded in meticulous detail and then transcribed to computer for exhaustive checking.
My starting point is an elegant proof by C. Thomassen [Am. Math. Mon. 99, No. 2, 116–130 (1992; Zbl 0773.57001)]. The proof first proves the Jordan curve theorem for polygons and then uses an approximation argument to derive the Jordan curve theorem in general.

MSC:
03B35 Mechanization of proofs and logical operations
57N05 Topology of the Euclidean \(2\)-space, \(2\)-manifolds (MSC2010)
57M15 Relations of low-dimensional topology with graph theory
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
HOL Light; Jordan; Mizar
PDF BibTeX XML Cite
Full Text: DOI