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

[Jesse Alama <alama@stanford.edu>]

Hi Adam,

I just wanted to write to congratulate you and all who have
collaborated to achieve this landmark of proof checking -- great work!

Warm regards,



Jesse

Adam Grabowski <adam@math.uwb.edu.pl> writes:

>   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

-- 
Jesse Alama (alama@stanford.edu)