The 6th Podlasie Conference on Mathematics (6PCM), hosted by the Polish Mathematical Society in cooperation with the Bialystok University of Technology and the University of Bialystok, will be held July 1-4, 2014, in Bialystok, Poland. This grant will provide support for six researchers from the United States to participate in the 6PCM Special Session organized by Artur Kornilowicz and entitled Computer-assisted Formalization of Mathematics --- In memoriam of Andrzej Trybulec. The special session, honoring the founder of Mizar, one of the earliest formalization systems, will be devoted to all aspects of computer-supported formalization of mathematics. The list of topics covered by the session includes: formalization of challenging mathematical problems, interactive and automated theorem proving, development of proof assistants, design of proof languages and techniques, repositories of formalized mathematics, semantic representation of mathematical knowledge, formal tools in program verification, foundations and philosophy of mathematics, and proof assistants in education.
Over the last decades, we witnessed a number of successful instances of computer-assisted formalization of mathematical problems. Research in this field has been boosted by the development of systems for practical formalization of mathematics (proof assistants), a creation of large repositories of computer-verified formal mathematics, and integration of interactive and automated methods of theorem proving. Proof assistants provide a very useful teaching tool suitable for undergraduate instruction, in particular for training beginning students in writing rigorous proofs. The meeting website is at http://katmat.pb.bialystok.pl/pcm14/
