Andrzej Trybulec
Andrzej W. Trybulec



Trybulec ca. 1975


Born  (19410129)January 29, 1941
Kraków, Poland

Died  September 11, 2013(20130911) (aged 72)
Białystok, Poland

Nationality  Polish 
Alma mater  University of Warsaw 
Known for  Mizar system Computeroriented formalization of mathematics 
Spouse(s)  Zinaida Trybulec 
Children  Wojciech A. Trybulec Michał J. Trybulec 
Awards  Kapitsa Medal, Russian Academy of Natural Sciences, 1995 Śleszyński Prize, Mizar Users Association, 1994 Golden Order of Merit, 1988 Silver Order of Merit, 1978 Golden Medal of Merit of the Warsaw Voivodeship, 1978 
Scientific career  
Fields  Mathematics Information Science Topology Computational linguistics Semantics 
Institutions  University of Białystok University of Warsaw Warsaw University of Technology Polish Academy of Sciences University of Connecticut AllRussian Scientific and Technical Information Institute 
Thesis  On some properties of the movable compacta (1975) 
Doctoral advisor  Karol Borsuk 
Notes  
Andrzej Wojciech Trybulec, (January 29, 1941 in Kraków, Poland – September 11, 2013 in Białystok, Poland) was a Polish mathematician and computer scientist noted for work on the Mizar system.^{[1]}
Early years
His parents Jan W. Trybulec and Barbara H. Kurlus both were professional pharmacists who owned a chemists shop in a small town Szczucin near the city of Tarnów in the southeastern Poland where they dispensed medicines. He went to high school in Ruda Śląska and then, on his own initiative, he transferred to a prestigious high school in Kraków, where he matriculated. He studied mathematics at the University of Warsaw, from 1964 to 1966 he lectured at the Chair of Geometry, in 1966 he graduated to the magister degree. Until 1967 he lectured at the Institute of Mathematics at the University of Warsaw, from 1967 to 1971 he was an assistant professor at the Warsaw University of Technology, since 1971 he worked at the Institute of Library and Information Science of the University of Warsaw. In September and October 1973, Trybulec was a visiting professor to the AllRussian Scientific and Technical Information Institute (VINITI) in Moscow, then the USSR, where he invented the idea of machinereadability of a mathematical text. He earned the doctoral degree in 1974 from the Institute of Mathematics of the Polish Academy of Sciences under Karol Borsuk.
Research work
Trybulec's first mathematical papers were in the various topological and metric space topics pioneered by Karol Borsuk. In parallel to his generic topological research, he also worked in computational linguistics and semantics of programming languages. Applying the framework of Tarski–Grothendieck set theory axioms, essentially the ZermeloFraenkel set theory supplemented by the Tarski axiom with all the objects being sets and eliminated notion of class, together with the firstorder logic of the GentzenJaśkowski natural deduction, in 1973 he designed the formalization system Mizar consisting of a formal language for writing mathematical definitions and proofs, a proof assistant, able to mechanically check proofs written in this language. Although the first presentation of the Mizar system on November 14, 1973 at a seminar in the Institute of Library Science and Scientific Information was an ideology understood as a visionary speculation rather than research project, his idea was later developed by himself and his collaborators to the Mizar Mathematical Library (MML), a library of formalized mathematics which can be used in the proof of new theorems and the world’s largest repository of formalized and computerchecked mathematics. Since 1978 until his death, he had lectured as a professor at the Institute of Computer Science at the University of Białystok, while in 19841985 hold visiting professorship at the Department of Computer Science and Engineering of the University of Connecticut. He published a number of articles, mostly with the journal Formalized Mathematics dedicated to MML contributions.
Publications
 Asperti, Andrea; Bancerek, Grzegorz; Trybulec, Andrzej, eds. (2004), Mathematical Knowledge Management: Proceedings of Third International Conference, MKM 2004, Białowieża, Poland, September 1921, 2004, Lecture Notes in Computer Science 3119, New York: Springer, ISBN 9783540230298
See also
 Mizar system
 Timeline of Polish science and technology
 List of Polish mathematicians
 List of Polish people
References
Further reading
 Kuperberg, Krystyna Trybulec (September 2015), "Andrzej Trybulec – in Memoriam", Journal of Automated Reasoning, 55 (3): 187–190, doi:10.1007/s1081701593433
 Matuszewski, Roman; Zalewska, Anna, eds. (2007), "From Insight to Proof: Festschrift in Honour of Andrzej Trybulec" (PDF), Studies in Logic, Grammar and Rhetoric, 10 (23), ISBN 9788374311281
 Matuszewski, Roman; Rudnicki, Piotr (March 2005), "Mizar: The first 30 years" (PDF), Mechanized Mathematics and its Applications, 4 (1): 3–24
 Rudnicki, Piotr (1992), "An overview of the MizarProject", in Nordström, Bengt; Petersson, Kent; Plotkin, Gordon (eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bästad, Sweden, June 1992, Båstad: Chalmers University of Technology, pp. 311–330
External links
 "Andrzej Trybulec", University of Bialystok
 Andrzej Trybulec at the Mathematics Genealogy Project
 Mizar System http://mizar.uwb.edu.pl
 http://math.uwb.edu.pl/~trybulec/awards.html
 https://web.archive.org/web/20060927204402/http://markun.cs.shinshuu.ac.jp/mizar/mma.dir/2005/mma2005(2).pdf
 http://wwwhistory.mcs.stand.ac.uk/Biographies/Kuperberg.html
 http://mizar.uwb.edu.pl/cgibin/andrzej/memento
 http://www.openmath.org/meetings/eindhoven2003/proceedings/trybulec.pdf
Copyright
 This page is based on the Wikipedia article Andrzej Trybulec; it is used under the Creative Commons AttributionShareAlike 3.0 Unported License (CCBYSA). You may redistribute it, verbatim or modified, providing that you comply with the terms of the CCBYSA.