[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] The proof of the Jordan Curve Theorem available in MML

  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.

The full Mizar article (MML Id: JORDAN) and its abstract can be browsed
online at
ftp://mizar.uwb.edu.pl/pub/version/mml/jordan.miz
ftp://mizar.uwb.edu.pl/pub/version/abstr/jordan.abs
(see also the link at the top of the Mizar home page
http://mizar.uwb.edu.pl/)

  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users