A complete proof of the Jordan Curve Theorem

    The Jordan Curve Theorem is an intuitively clear theorem that in rough terms states, "A closed curve divides a plane into the inside and outside areas" (see figure below).

    Camille Jordan (see) stated in his publications in 1887 that "this theorem is clearly true", but it was later discovered that the proof of the theorem is in fact quite difficult.
    Oswald Veblen is said to have proved the theorem to some extent in 1905, but the proof relies on intuition in a number of places in the assumed knowledge so it cannot be called a complete proof.
    In many areas of mathematics and science (theory of complex functions, electromagnetics, the four color problem, etc.), the Jordan Curve Theorem is assumed inexplicitly and sometimes explicitly.
    Since then, many books and papers have been published concerning the Jordan Curve Theorem, but in many cases they introduce references to other books and papers and upon searching the references, these in turn introduce yet further references and at some point the deepest link of references is lost.
    It was clear from the start that the only way to construct a complete proof of the theorem was to build the proofs of all of the necessary mathematics from the foundation level without skipping any steps based on intuition. It was at this time of progress of computers in the background in which the development of proof checker systems began to appear. In these proof checker systems, mathematical proofs written by humans in a specified grammar are checked by computers.
    Since computers must follow strict rules, skipping steps in a proof based on the reason that they are intuitive is not tolerated. The most well-known of these is the proof checker system called Mizar created by the team of researchers under Dr. Andrzej Trybulec in Poland.
    Yatsuka Nakamura of Japan also created an original proof checker, but made the decision to join efforts with the team from Poland and undertake a large work of Mizar in constructing the complete proof of the Jordan Curve Theorem in a colloborative project between Japan and Poland.
    The time was 1991. Agata Darmochwal of the Bialystok branch of Warsaw University first visited Shinshu University and wrote the article called TOPREAL1 with Dr. Nakamura. This opportunity provided the catalyst for more than 10 mathematicians from Japan and Poland to join the project of dividing into pieces and constructing the entire proof. The paper which provided the direction of the proof was written by Yukio Takeuchi former professor of Shinshu University (this proof still contained many portions of intuition which needed to be resolved, but the intuitive portions were fewer in number than in other proofs).
    Finally, in September 2005, the final piece of the proof was completed by Dr. Artur Kornilowicz and the project which spanned 14 years was brought to a close on a successful note.
    By compiling the proofs of all the divided pieces done by the team members, the complete assembled proof turned out to require 200,000 lines. As well as demonstrating the difficulty and involvement of complete logical reasoning, this work also shows the potential of Mizar by accomplishing a major piece of mathematical work. As a result of the culmination of this complete proof of the Jordan Curve Theorem, Mizar will be sure to gain recognition around the world as a new method for mathematics and reasoning.
    Finally, I would like to include the message from Dr. Adam Grabowski posted to the mailing list detailing the accomplishments of the Jordan Curve Theorem project by the Mizar group.

September 26, 2005 Yatsuka Nakamura

Dear All,

I have the great pleasure to announce on behalf of the Mizar team, that with the submission of Artur Kornilowicz's article JORDAN (now available in the current version of MML) we have finally completed formalizing in Mizar the proof of the Jordan Curve Theorem. You may want to know that the actual formalization of the theorem started in 1992, preceded by some preliminary works devoted to the topology of the plane. Since that time, almost a hundred of Mizar articles were created, directly or indirectly devoted to the project, comprising now about 10 per cent of the whole library. The growth of various other branches of MML has been highly stimulated by this development, to mention only fields like general topology, the theory of finite sequences, etc.

Therefore special thanks are due to Prof. Yatsuka Nakamura for introducing the challenging topic and his continual commitment into its realization, and Prof. Andrzej Trybulec for coordinating the project in Poland and his guidance in all the stages of the development. It should also be underlined that the project established a long lasting cooperation between Shinshu University and the University of Bialystok, since much of the formalization was done as collaborative work, thanks to numerous research visits in Japan and Poland. We hope that the fruitful cooperation initialized by this project will continue also in other fields.

Once again many thanks to all the people whose work directly contributed to the project (in alphabetic order): Grzegorz Bancerek, Jozef Bialas, Czeslaw Bylinski, Agata Darmochwal, Mariusz Giero, Adam Grabowski, Artur Kornilowicz, Jaroslaw Kotowicz, Roman Matuszewski, Robert Milewski, Yatsuka Nakamura, Adam Naumowicz, Yasunari Shidama, Andrzej Trybulec, and Mariusz Zynel. (And Piotr Rudnicki, added by Y.Nakamura)

Adam Grabowski
Library Committee of the Association of Mizar Users

Mathematics is alive