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.
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)
Regards,
Adam Grabowski
Library Committee of the Association of Mizar Users