Adam Naumowicz

• Education and interests
• List of publications
• Information for students
• Personal information
• Contact

• Automated proof checking and theorem proving (development of the Mizar system)
• Computer aided formalization of mathematics (development of Mizar Mathematical Library)
• Formal methods in computer science education
• Also: general topology, continuous lattices, algebraic geometry

Formalized Mathematics Editor	Journal of Formalized Reasoning Editor	Central European Journal of Computer Science (currently: Open Computer Science) Managing Editor (2010-2014)	Studies in Logic, Grammar and Rhetoric Guest Editor for a special issue on Computer Reconstruction of the Body of Mathematics	Conferences on Intelligent Computer Mathematics PC Member CICM 2015, July 13-17, 2015 Washington DC, USA

• Programming: Pascal, C, C++, Java, Perl
• OS administration: Linux (Red Hat Certified Technician (RHCT) and Red Hat Certified Engineer (RHCE) for Red Hat Enterprise Linux 5), FreeBSD, Solaris
• Languages: Polish (native), English, Russian

• SONALF, EuroProofNet School on Natural Formal Mathematics, June 3-5, 2025, Bonn, Germany [download slides]
• CICM 2023, 16th Conference on Intelligent Computer Mathematics, September 4-8, 2023, Cambridge, UK (Programme Committee member) [download slides]
• ITP 2023, 14th International Conference on Interactive Theorem Proving, July 31-August 4, 2023, Bialystok, Poland (Programme Committee co-Chair)
• ITP 2022, 13th International Conference on Interactive Theorem Proving, August 7-10, 2022, Haifa, Israel (Programme Committee member)
• Machine-Checked Mathematics, March 2-4, 2022, Leiden, The Netherlands (online workshop) [download slides]
• CICM 2021, 14th Conference on Intelligent Computer Mathematics, July 26-31, 2021, Timisoara, Romania (online conference) (Programme Committee member)
• ITP 2021, 12th International Conference on Interactive Theorem Proving, June 29-July 1, 2021, Rome, Italy (online conference) (Programme Committee member) [download slides]
• SYNASC 2020, 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, September 1-4, 2020, Timisoara, Romania (online conference) [download slides]
• CICM 2020, 13th Conference on Intelligent Computer Mathematics, July 26-31, 2020, Bertinoro, Forli, Italy (online conference) (Programme Committee member) [download slides]
• CICM 2019, 12th Conference on Intelligent Computer Mathematics, July 8-12, 2019, Prague, Czech Republic (Programme Committee member, co-organizer of the tutorial 'Exploring the Mizar Mathematical Library')
• FMM 2019, Forth Workshop on Formal Mathematics for Mathematicians, July 8, 2019, Prague, Czech Republic [download slides]
• CICM 2018, 11th Conference on Intelligent Computer Mathematics, August 13-17, 2018, Hagenberg, Austria (Programme Committee member) [download slides]
• FMM 2018, Third Workshop on Formal Mathematics for Mathematicians, August 13, 2018, Hagenberg, Austria (Co-chair)
• COST Action CA15123 EUTypes Short-Term Scientific Mission (STSM) at Czech Institute of Informatics, Robotics and Cybernetics, Czech Technical University in Prague, Czech Republic - 'Study of machine-learning techniques over formal mathematics in Mizar', March 8-14, 2018
• ITP 2017, 8th International Conference on Interactive Theorem Proving, September 26-29, 2017, Brasilia, Brazil [download slides]
• ISAT 2017, 38th International Conference on Information Systems Architecture and Technology, September 17-19, 2017, Szklarska Poreba, Poland [download slides]
• CICM 2017, 10th Conference on Intelligent Computer Mathematics, July 17-21, 2017, Edinburgh, Scotland (Programme Committee member of the MKM track)
• TYPES 2017, 23rd International Conference on Types for Proofs and Programs, May 29 - Jun 1, 2017, Budapest, Hungary [download slides]
• Dagstuhl Seminar on Universality of Proofs, October 16-21, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany
• CICM 2016, 9th Conference on Intelligent Computer Mathematics, July 25-29, 2016, Bialystok, Poland (Conference Chair and Programme Committee member of the FMM workshop)
• TYPES 2016, 22nd International Conference on Types for Proofs and Programs, May 23-26, 2016, Novi Sad, Serbia [download slides]
• CICM 2015, Conference on Intelligent Computer Mathematics, July 13-17, 2015, Washington, USA (Programme Committee member of the Systems & Data track and the FMM workshop)
• CICM 2014, Conferences on Intelligent Computer Mathematics, July 7-11, 2014, Coimbra, Portugal (Programme Committee member of the MKM and Calculemus tracks)
• ESSLLI 2012, 24th European Summer School in Logic, Language and Information ESSLLI 2012, August 6-17, 2012, Opole, Poland (Course: An Introduction to Computer Formalization of Mathematics)
• CICM 2012, Conferences on Intelligent Computer Mathematics, July 8-13, 2012, Bremen, Germany (Programme Committee member of the MKM track and UITP workshop)
• AIPA 2012, Automation in Proof Assistants 2012, March 31 - April 1, 2012, Tallinn, Estonia (Programme Committee member)
• CADE 23, The 23rd International Conference on Automated Deduction, July 31-August 5, 2011, Wroclaw, Poland (Organizer of the tutorial Practical Computer Formalization of Mathematics Using Mizar)
• CICM 2011, Conference on Intelligent Computer Mathematics, July 18-23, 2011, Bertinoro, Italy (Programme Committee member)
• AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics, New Orleans, USA, January 6-9, 2011
• TYPES 2010, The 17th Workshop Types for Proofs and Programs, October 13-16, 2010, Warsaw, Poland
• MKM 2010, The 9th International Conference on Mathematical Knowledge Management - as part of Conferences on Intelligent Computer Mathematics (CICM 2010) - July 5-10, 2010, Paris, France (Programme Committee member)
• Cooperative research at Shinshu University, Nagano, Japan, February 2-28, 2010
• Third Indian School on Logic and its Applications, January 18-29, 2010, University of Hyderabad, Gachibowli, India, [download slides]
• TPHOLs 2009, Theorem Proving in Higher Order Logics, 17-20 August, 2009, Munich, Germany [download slides]
• ETAPS 2008 satellite event Formal Methods in Computer Science Education (FORMED2008), March 29, 2008, Budapest, Hungary [download slides]
• TYPES topical workshop MathWiki, October 31 - November 1, 2007, Edinburgh, UK [download slides]
• TYPES Summer School 2007, August 19-31, 2007, Bertinoro, Italy [download slides]
• RDP 2007 affiliated TYPES Workshop on Proof Assistants and Types in Education, June 25, 2007, Paris, France (Programme Committee member)
• TYPES 2006, Conference of the TYPES Project, April 18-21, 2006, Nottingham, UK
• TYPES Summer School 2005, Proofs of Programs and Formalisation of Mathematics, August 15-26, 2005, Goteborg, Sweden
• MKM 2005, Fourth International Conference on Mathematical Knowledge Management, July 15-17, 2005, Bremen, Germany
• Small TYPES Workshop: High Level Languages for Proofs, April 13-14, 2005, Chambery, France [download slides]
• MKM 2004, Third International Conference on Mathematical Knowledge Management, September 19-21, 2004, Bialowieza, Poland
• The Prague 2004 Workshop on Knowledge Management in Formalized Mathematics, June 27-29, 2004, Prague, Czech Republic
• MKM Symposium, November 25-29, 2003, Edinburgh, UK
• CALCULEMUS 2003, 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, September 10-12, 2003, Rome, Italy
• MONET 2003, Mathematics on the Semantic Web, May 12-14, 2003, Eindhoven, The Netherlands
• TYPES 2003, Workshop of the TYPES Working Group, April 30 - May 4, 2003, Turin, Italy
• TYPES 2002, Workshop of the TYPES Working Group, April 24-28, 2002, Berg en Dal (near Nijmegen), The Netherlands
• Cooperative research at Shinshu University, Nagano, Japan - 'Verification of Circuit designs with the Aid of the Mizar System', January 1 - March 12, 2002
• CALCULEMUS 2001, 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, June 21-22, 2001, Siena, Italy

• Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), member of the Board of Control

• 2017-2018: NCN Grant DEC-2017/01/X/STG/00012
• 2009-2011: MNiSW Grant N519 385136
• 2004-2008: TYPES II EU FP6 510996
• 2003-2006: KBN Grant 4 T11C 039 24
• 2000-2004: CALCULEMUS EU FP5 HPRN-CT-2000-00102
• 2000-2003: TYPES EU FP5 IST-1999-29001
• 1997-1998: ONR Grant N00014-97-1-0777
• 1997-1998: KBN Grant 8 T11C 018 12

• Adam Naumowicz. Elementary Number Theory Problems. Part XI . Formalized Mathematics 31(1), pp. 229-275, 2023
• Adam Naumowicz. Extending Numeric Automation for Number Theory Formalizations in Mizar. In: Dubois C. and Kerber M. (Eds.), Intelligent Computer Mathematics, CICM 2023, LNCS 14101, pp. 309-314, 2023
• Adam Naumowicz, Rene Thiemann (Eds.), 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bialystok, Poland. LIPIcs 268, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik 2023, ISBN 978-3-95977-284-6
• Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Muller, Yasmine Sharoda, Claudio Sacerdoti Coen (Eds.), Joint Proceedings of the FMM, FVPS, MathUI, NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021. CEUR Workshop Proceedings 3377, CEUR-WS.org 2023
• Artur Kornilowicz, Adam Naumowicz. Elementary Number Theory Problems. Part V . Formalized Mathematics 30(3), pp. 229-234, 2022
• Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz. Syntactic-semantic Form of Mizar Articles. In: Cohen, L., Kaliszyk, C. (Eds.), 12th International Conference on Interactive Theorem Proving, ITP 2021, pp. 11.1-11.17, 2021
• Adam Naumowicz. An Experiment on Mizar Adjectives with Extra Visible Arguments. In: 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2020, pp. 97-100, 2020
• Adam Naumowicz. Dataset Description: Formalization of Elementary Number Theory in Mizar. In: Benzmuller C., Miller B. (Eds.), Intelligent Computer Mathematics, CICM 2020, LNCS 12236, pp. 303-308, 2020
• Adam Naumowicz. Elementary Number Theory Problems. Part I . Formalized Mathematics 28(1), pp. 115-120, 2020
• Adam Naumowicz. Testing Mizar User Interactivity in a University-level Introductory Course on Foundations of Mathematics. In E. Brady et al. (Eds.), Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019, CEUR-WS Vol-2634, 2020
• Grzegorz Bancerek, Adam Naumowicz, Josef Urban. System Description: XSL-Based Translator of Mizar to LaTeX. In F. Rabe et al. (Eds.), Intelligent Computer Mathematics, CICM 2018, LNCS 11006, pp. 1-6, 2018
• Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. Journal of Automated Reasoning 61(9), pp. 9-32, 2018
• Adam Naumowicz, Artur Kornilowicz. Introducing Euclidean Relations to Mizar. Proceedings of the 2017 Federated Conference on Computer Science and Information Systems (FedCSIS), Annals of Computer Science and Information Systems vol. 11, pp. 245-248, 2017
• Artur Kornilowicz, Adam Naumowicz, Adam Grabowski. All Liouville Numbers are Transcendental. Formalized Mathematics 25(1), pp. 49-54, 2017
• Adam Naumowicz. Towards Standardized Mizar Environments. Information Systems Architecture and Technology, Proceedings of 38th International Conference on Information Systems Architecture and Technology, ISAT 2017, part II, pp. 166-175, 2017
• Adam Naumowicz. Adjective clustering in the Mizar type system. Proceedings of the 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
• Artur Kornilowicz, Adam Naumowicz. Niven's Theorem. Formalized Mathematics 24(4), pp. 301-308, 2016
• Adam Naumowicz, Radoslaw Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar Parser. In M. Kohlhase et al. (Eds.), Intelligent Computer Mathematics, CICM 2016, LNAI 9791, pp. 77-82, 2016
• Adam Naumowicz. Linking to Compound Conditions in Mizar. In M. Kohlhase et al. (Eds.), Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016, CEUR-WS Vol-1785, 2017
• Adam Naumowicz. Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver. Journal of Automated Reasoning 55(3), pp. 285-294, 2015
• Adam Grabowski, Artur Kornilowicz, Adam Naumowicz. Four Decades of Mizar - Foreword. Journal of Automated Reasoning 55(3), pp. 191-198, 2015
• Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban. Mizar: State-of-the-Art and Beyond. In M. Kerber et al. (Eds.), Intelligent Computer Mathematics, CICM 2015, LNAI 9150, pp. 261-279, 2015
• Adam Naumowicz. Tools for MML Environment Analysis. In M. Kerber et al. (Eds.), Intelligent Computer Mathematics, CICM 2015, LNAI 9150, pp. 348-352, 2015
• Adam Naumowicz. SAT-Enhanced Mizar Proof Checking. In S. Watt et al. (Eds.), Intelligent Computer Mathematics, CICM 2014, LNCS 8543, pp. 449-452, 2014
• Adam Naumowicz. A Note on the Seven Bridges of Koenigsberg Problem. Formalized Mathematics 22(2), pp. 177-178, 2014
• Valerie Novitzka, William Steingartner, Adam Naumowicz (Eds.). Selected papers from the International Scientific Conference INFORMATICS'2013 - part II. Central European Journal of Computer Science 4(4), p. 203, 2014
• Valerie Novitzka, William Steingartner, Adam Naumowicz (Eds.). Selected papers from the International Scientific Conference INFORMATICS'2013 - part I. Central European Journal of Computer Science 4(3), p. 95, 2014
• Adam Naumowicz, Radoslaw Piliszek. Mizar Formalization of Divisibility Rules. Mechanized Mathematics and Its Applications, Vol. 9, No. 1-2, pp. 11-17, Mizar Japan, 2014
• Adam Naumowicz, Radoslaw Piliszek. More on Divisibility Criteria for Selected Primes. Formalized Mathematics 21(2), pp. 87-94, 2013
• Andrzej Trybulec, Artur Kornilowicz, Adam Naumowicz, Krystyna Kuperberg (Eds.). Formal Mathematics for Mathematicians. Journal of Automated Reasoning 50(2), 2013
• Andrzej Trybulec, Artur Kornilowicz, Adam Naumowicz, Krystyna Kuperberg. Formal Mathematics for Mathematicians. Foreward to the Special Issue. Journal of Automated Reasoning 50(2), pp.119-121, 2013
• Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban. Licensing the Mizar Mathematical Library. In J. Davenport et al. (Eds.), CALCULEMUS/MKM 2011, LNAI 6824, pp. 149-163, Springer-Verlag Berlin Heidelberg, 2011
• Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama. Partial Differentiation, Differentiation and Continuity on n-Dimensional Real Normed Linear Spaces. Formalized Mathematics 19(2), pp. 65-68, 2011
• Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama. Partial Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces. Formalized Mathematics 19(1), pp. 1-9, 2011
• Adam Grabowski, Artur Kornilowicz, Adam Naumowicz. Mizar in a Nutshell. In A. Asperti, J. Harrison and C. Munoz (Eds.) User Tutorials I. Journal of Formalized Reasoning 3(2), pp. 153-245, 2010.
• Adam Naumowicz. Interfacing External CA Systems for Gröbner Bases Computation in Mizar Proof Checking. International Journal of Computer Mathematics 87(1), pp. 1-11, 2010
• Adam Grabowski, Adam Naumowicz (Eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric 18(31), 2009
• Adam Naumowicz. Enhanced Processing of Adjectives in Mizar. In A. Grabowski and A. Naumowicz (Eds.), Computer Reconstruction of the Body of Mathematics, Studies in Logic, Grammar and Rhetoric 18(31), pp. 89-101, 2009
• Adam Naumowicz, Artur Kornilowicz. A Brief Overview of Mizar. In S. Berghofer et al. (Eds.), TPHOLs 2009, LNCS 5674, pp. 67-72, Springer-Verlag Berlin Heidelberg, 2009
• Adam Naumowicz. Teaching How to Write a Proof. In Proceedings of ETAPS 2008 satellite workshop Formal Methods in Computer Science Education (FORMED2008) pp. 91-100, Budapest, March 29, 2008
• Adam Naumowicz. Formalization of the Tietze Extension Theorem in Mizar. Mechanized Mathematics and Its Applications, Vol. 6, No. 1, pp. 41-45, Mizar Japan, 2007
• Adam Naumowicz. Evaluating Prospective Built-in Elements of Computer Algebra in MIZAR. In R. Matuszewski and A. Zalewska (Eds.), From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric 10(23), pp. 191-200, 2007
• Adam Naumowicz. How to Teach to Write a Proof. In Proceedings of RDP 2007 affiliated TYPES Workshop on Proof Assistants and Types in Education, pp. 69-76, Paris, June 25, 2007
• Adam Naumowicz. An Example of Formalizing Recent Mathematical Results in MIZAR. In C. Benzmueller (Ed.), Towards Computer Aided Mathematics, Journal of Applied Logic, 4(4), pp. 396-413, Elsevier, 2006
• Adam Naumowicz. On the Representation of Natural Numbers in Positional Numeral Systems. Formalized Mathematics, 14(4), pp. 221-223, 2006
• Adam Naumowicz, Grzegorz Bancerek. Homeomorphisms of Jordan Curves. Formalized Mathematics, 13(4), pp. 477-480, 2005
• Artur Kornilowicz, Grzegorz Bancerek, Adam Naumowicz. Tietze Extension Theorem. Formalized Mathematics, 13(4), pp. 471-475, 2005
• Adam Naumowicz. Spaces of Pencils, Grassmann Spaces, and Generalized Veronese Spaces. Formalized Mathematics, 13(1), pp. 133-138, 2005
• Adam Naumowicz. On the Characterisation of Collineations of the Segre Product of Strongly Connected Partial linear Spaces. Formalized Mathematics, 13(1), pp. 125-131, 2005
• Adam Naumowicz, Czeslaw Bylinski. Improving MIZAR Texts with Properties and Requirements. In A. Asperti et al. (Eds.), MKM 2004, LNCS 3119, pp. 290-301, Springer-Verlag Berlin Heidelberg, 2004
• Adam Naumowicz, Krzysztof Prazmowski. The Geometry of Generalized Veronese Spaces. Results in Mathematics, vol. 45, pp. 115-136, Birkhauser Verlag, 2004
• Adam Naumowicz, Czeslaw Bylinski. Basic Elements of Computer Algebra in MIZAR. Mechanized Mathematics and Its Applications, Vol. 2, pp. 9-16, Mizar Japan, 2002
• Grzegorz Bancerek, Adam Naumowicz. Preliminaries to Automatic Generation of Mizar Documentation for Circuits. Formalized Mathematics, 10(3), pp. 117-133, 2002
• Adam Naumowicz, Robert Milewski. Some Remarks on Clockwise Oriented Sequences on Go-boards. Formalized Mathematics, 10(1), pp. 23-27, 2002
• Adam Naumowicz, Krzysztof Prazmowski. On Segre's product of partial line spaces and spaces of pencils. Journal of Geometry, vol. 71, pp. 128-143, Birkhauser Verlag, 2001
• Adam Naumowicz. On cosets in Segre's product of partial linear spaces. Formalized Mathematics, 9(4), pp. 801-806, 2001
• Adam Naumowicz. Some remarks on finite sequences on Go-boards. Formalized Mathematics, 9(4), pp. 821-824, 2001
• Artur Kornilowicz, Robert Milewski, Adam Naumowicz, Andrzej Trybulec. Some properties of cells and arcs. Formalized Mathematics, 9(3), pp. 535-539, 2001
• Artur Kornilowicz, Robert Milewski, Adam Naumowicz, Andrzej Trybulec. Gauges and cages.Part I. Formalized Mathematics, 9(3), pp. 505-513, 2001
• Adam Naumowicz. Segre's product of partial line spaces. Formalized Mathematics, 9(2), pp. 383-390, 2001
• Grzegorz Bancerek, Adam Naumowicz. The characterization of the continuity of topologies. Formalized Mathematics, 9(2), pp. 231-236, 2001
• Adam Naumowicz. A note on affine partial linear spaces. Geometria Wykreslna i Grafika Inzynierska (Descriptive geometry and engineering graphics) Zeszyt nr. 5, ISSN 1425-333X, pp. 57-62, Wroclaw Technical University, 2000
• Grzegorz Bancerek, Adam Naumowicz. Function spaces in the category of directed suprema preserving maps. Formalized Mathematics, 9(1), pp. 171-176, 1999
• Adam Naumowicz, Agnieszka Julia Marasik. The correspondence between lattices of subalgebras of universal algebras and many sorted algebras. Formalized Mathematics, 7(2), pp. 227-231, 1998
• Adam Naumowicz. On the characterization of modular and distributive lattices. Formalized Mathematics, 7(1), pp. 53-55, 1998
• Adam Naumowicz, Mariusz Lapinski. On T_1 reflex of topological space. Formalized Mathematics, 7(1), pp. 31-34, 1998
• Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2), pp. 265-268, 1997

• Programowanie Strukturalne (in Polish)
• Podstawy Logiki i Teorii Mnogosci (in Polish)
• Systemy operacyjne (in Polish)
• Programowanie niskopoziomowe (Assembler) (in Polish)
• Programowanie w internecie (in Polish)
• Information Technology as a Tool for Self-Education

---

Contact adamn@math.uwb.edu.pl

---

Last modification : Tue Jun 17 12:55:44 2025 GMT
This page has been accessed 62721 times.