Computer-assisted Formalization of Mathematics, 6th Podlasie Conference, Bialystok, July 1-4, 2014

第六届Podlasie数学会议（6PCM），由波兰数学学会与技术比亚韦斯托克大学和比亚韦斯托克大学合作主办，将于2014年7月1日至4日在比亚韦斯托克，波兰举行。这笔赠款将支持来自美国的六名研究人员参加Artur Kornilowicz组织的6PCM特别会议，题为计算机辅助数学形式化-纪念Andrzej Trybulec。 特别会议，纪念Mizar的创始人，最早的形式化系统之一，将致力于计算机支持的数学形式化的各个方面。会议涵盖的主题清单包括：具有挑战性的数学问题的形式化，交互式和自动化定理证明，证明助手的开发，证明语言和技术的设计，形式化数学的知识库，数学知识的语义表示，程序验证中的形式化工具，数学的基础和哲学，以及教育中的证明助手。在过去的几十年里，我们目睹了一些计算机辅助数学问题形式化的成功实例。这一领域的研究得到了数学实用形式化系统（证明助手）的发展，计算机验证的形式数学的大型知识库的创建，以及定理证明的交互式和自动化方法的集成。证明助理提供了一个非常有用的教学工具，适合本科教学，特别是培训开始学生在写作严格的证明。会议网址为http://katmat.pb.bialystok.pl/pcm14/

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/