Recent publications:

1. Cezary Kaliszyk, Karol Pąk, Combining Higher-Order Logic with Set Theory Formalizations, Journal of Automated Reasoning, 67(2):1--20, 2023.
   [BibTex, Publisher's site, PDF(openaccess)]
2. Karol Pąk, Cezary Kaliszyk, Formalizing a Diophantine Representation of the Set of Prime Numbers, Thirteenth International Conference, Interactive Theorem Proving, ITP 2022, Haifa, Israel, 2022, August 7-10, 2022. Proceedings, volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1--26:8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
   [BibTex, Publisher's site, PDF(openaccess)]
3. Cezary Kaliszyk, Karol Pąk, Declarative Proof Translation, Tenth International Conference, Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 8-13, 2019. Proceedings, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:7. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
   [BibTex, Publisher's site, PDF(openaccess)]
4. Chad E. Brown, Cezary Kaliszyk, Karol Pąk, Higher-order Tarski Grothendieck as a Foundation for Formal Proof, Tenth International Conference, Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 8-13, 2019. Proceedings, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
   [BibTex, Publisher's site, PDF(openaccess)]
5. Chad E. Brown, Karol Pąk, A Tale of Two Set Theories, Intelligent Computer Mathematics In C. Kaliszyk and E. Brady and A. Kohlhase and C. Sacerdoti Coen editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44-60. Springer, 2019.
   [BibTex, Publisher's site, PDF (preprint)]

Publications:

The Mizar System in the Isabelle Logical Framework:

• Cezary Kaliszyk, Karol Pąk, Combining Higher-Order Logic with Set Theory Formalizations, Journal of Automated Reasoning, 67(2):1--20, 2023.
  [BibTex, Publisher's site, PDF(openaccess)]
• Cezary Kaliszyk, Karol Pąk, Declarative Proof Translation (Short Paper), Tenth International Conference, Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 8-13, 2019. Proceedings, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:7. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
  [BibTex, Publisher's site, PDF(openaccess)]
• Chad E. Brown, Cezary Kaliszyk, Karol Pąk, Higher-order Tarski Grothendieck as a Foundation for Formal Proof, Tenth International Conference, Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 8-13, 2019. Proceedings, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
  [BibTex, Publisher's site, PDF(openaccess)]
• Chad E. Brown, Karol Pąk, A Tale of Two Set Theories, Intelligent Computer Mathematics In C. Kaliszyk and E. Brady and A. Kohlhase and C. Sacerdoti Coen editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44-60. Springer, 2019.
  [BibTex, Publisher's site, PDF (preprint)]
• Cezary Kaliszyk, Karol Pąk, Semantics of Mizar as an Isabelle Object Logic, 2018.
  [BibTex, Publisher's site, PDF(openaccess)]
• Cezary Kaliszyk, Karol Pąk, Isabelle Import Infrastructure for the Mizar Mathematical Library, In F. Rabe and W. M. Farmer and G. O. Passmore and A. Youssef, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pages 131-146. Springer, 2018.
  [BibTex, Publisher's site, PDF (preprint)]
• Karol Pąk, Combining the Syntactic and Semantic Representations of Mizar Proofs, In M. Ganzha, L. A. Maciaszek, M. Paprzycki, Federated Conference on Computer Science and Information Systems, FedCSIS 2018, Poznan, Poland, September 9-12, 2018, volume 15 of Annals of Computer Science and Information Systems, pages 145-153.
  [BibTex, Publisher's site , PDF(openaccess), PDF]
• Cezary Kaliszyk, Karol Pąk, Isabelle Formalization of Set Theoretic Structures and Set Comprehensions, In J. Blömer, I. S. Kotsireas, T. Kutsia, D. E. Simos editors, 7th International Conference, Mathematical Aspects of Computer and Information Sciences, MACIS 2017, Vienna, Austria, November 15-17, 2017, Proceedings volume 10693 of Lecture Notes in Computer Science, pages 163-178. Springer, 2017.
  [BibTex, Publisher's site, PDF (preprint)]
• Cezary Kaliszyk, Karol Pąk, Progress in the Independent Certification of Mizar Mathematical Library in Isabelle, In M. Ganzha, L. A. Maciaszek, M. Paprzycki, Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Praga, Czech Republic, September 3-6, 2017, volume 11 of Annals of Computer Science and Information Systems, pages 227-236.
  [BibTex, Publisher's site , PDF(openaccess)]
• Cezary Kaliszyk, Karol Pąk, Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic, In H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, editors, Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, volume 10383 of Lecture Notes in Computer Science, pages 193-207. Springer, 2017.
  [BibTex, Publisher's site, PDF (preprint)]
• Karol Pąk, Mizar Set Comprehension in Isabelle Framework, In M. Ganzha, L. A. Maciaszek, M. Paprzycki, Federated Conference on Computer Science and Information Systems, FedCSIS 2018, Poznan, Poland, September 9-12, 2018, volume 15 of Annals of Computer Science and Information Systems, pages 23-26.
  [BibTex, Publisher's site , PDF(openaccess), PDF]
• Cezary Kaliszyk, Karol Pąk, Josef Urban, Towards a Mizar Environment for Isabelle: Foundations and Language, In J. Avigad and A. Chlipala, editors, Proceedings, 5th Conference on Certified Programs and Proofs (CPP 2016), pages 58-65. ACM, 2016.
  [BibTex, Publisher, PDF(openaccess)]

Improving Legibility of Formal Proofs:

• Karol Pąk, Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-hard, Journal of Automated Reasoning, 55(3):295--306, 2015.
  [BibTex, Publisher's site, PDF(openaccess)]
• Karol Pąk, Improving Legibility of Natural Deduction Proofs is not Trivial Logical Methods in Computer Science, 10(3), 2014.
  [BibTex, arXiv, PDF(openaccess)]
• Karol Pąk, Automated Improving of Proof Legibility in the Mizar System. In S. M. Watt, J. H. Davenport, A. P. Sexton, P. Sojka, and J. Urban, editors, Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings, volume 8543 of Lecture Notes in Computer Science, pages 373-387. Springer, 2014.
  [BibTex, Publisher's site, PDF(preprint)]
• Karol Pąk, Methods of Lemma Extraction in Natural Deduction Proofs. Journal of Automated Reasoning, 50(2):217-228, 2013.
  [BibTex, Publisher's site, PDF(openaccess)]
• Karol Pąk, Improving Legibility of Proof Scripts Based on Quantity of Introduced Labels. In A. Gomolińska, A. Grabowski, M.Hryniewicka, M. Kacprzak, and E. Schmeidel, editors, Trends in Contemporary Computer Science Podlasie 2014, pages 71-82. Bialystok University of Technology Publishing Office, 2014.
  [BibTex, Publisher, PDF(openaccess)]
• Karol Pąk, Lemma Extraction Criteria Based on Properties of Theorem Statements, In A. Kohlhase, P. Libbrecht, B. R. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. W. Tompa, and M. Suda, editors, Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016., volume 1785 of CEUR Workshop Proceedings, pages 158-171. CEUR-WS.org, 2016.
  [BibTex, Publisher's site, PDF(openaccess)]
• Karol Pąk, Aleksy Schubert, The Impact of Proof Steps Sequence on Proof Readability - Experimental Setting, In A. Kohlhase, P. Libbrecht, B. R. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. W. Tompa, and M. Suda, editors, Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016., volume 1785 of CEUR Workshop Proceedings, pages 172-186. CEUR-WS.org, 2016.
  [BibTex, Publisher's site, PDF(openaccess)]
• Karol Pąk, The Algorithms for Improving and Reorganizing Natural Deduction Proofs. Studies in Logic, Grammar and Rhetoric, 22(35):95-112, 2010.
  [BibTex, Publisher's site, PDF(openaccess)]

Described Formalizations:

• Karol Pąk, Cezary Kaliszyk, Formalizing a Diophantine Representation of the Set of Prime Numbers, Thirteenth International Conference, Interactive Theorem Proving, ITP 2022, Haifa, Israel, 2022, August 7-10, 2022. Proceedings, volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1--26:8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.
  [BibTex, Publisher's site, PDF(openaccess)]
• Marcin Acewicz, Karol Pąk, Formalization of Pell`s Equations in the Mizar System, In M. Ganzha, L. A. Maciaszek, M. Paprzycki, editors, Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Praga, Czech Republic, September 3-6, 2017, volume 11 of Annals of Computer Science and Information Systems, pages 223-226.
  [BibTex, Publisher's site, PDF(openaccess)]
• Karol Pąk, Readable Formalization of Euler's Partition Theorem in Mizar In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, volume 9150 of Lecture Notes in Computer Science, pages 211-226. Springer, 2015.
  [BibTex, Publisher's site, PDF(preprint)]
• Karol Pąk Topological Foundations for a Formal Theory of Manifolds , In A. Kohlhase, P. Libbrecht, B. R. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. W. Tompa, and M. Suda, editors, Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016., volume 1785 of CEUR Workshop Proceedings, pages 14-16. CEUR-WS.org, 2016.
  [BibTex, Publisher's site, PDF(openaccess)]

Formalized Mathematics:

1. 2022
   • Karol Pąk, Prime Representing Polynomial with 10 Unknowns, Formalized Mathematics, 30(4), 255 - 279, 2022.
     [BibTex, sciendo(openaccess) ]
   • Karol Pąk, Prime Representing Polynomial with10 Unknowns – Introduction. Part II, Formalized Mathematics, 30(4), 245 - 253, 2022.
     [BibTex, sciendo(openaccess) ]
   • Karol Pąk, Prime Representing Polynomial with 10 Unknowns – Introduction, Formalized Mathematics, 30(3), 169 - 198, 2022.
     [BibTex, sciendo(openaccess) ]
2. 2021
   • Karol Pąk, Prime Representing Polynomial, Formalized Mathematics, 29(4), 221 - 228, 2021.
     [BibTex, sciendo(openaccess) ]
3. 2020
   • Karol Pąk, Grothendieck Universes, Formalized Mathematics, 28(2), 211 - 215, 2020.
     [BibTex, sciendo(openaccess) ]
4. 2019
   • Karol Pąk, Formalization of the MRDP Theorem in the Mizar System, Formalized Mathematics, 27(2), 209 - 222, 2019.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Diophantine Sets. Part II, Formalized Mathematics, 27(2), 197-209, 2019.
     [BibTex, sciendo(openaccess)]
5. 2018
   • Marcin Acewicz, Karol Pąk, Basic Diophantine Relations, Formalized Mathematics, 26(2), 175-181, 2018.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Diophantine sets. Preliminaries, Formalized Mathematics, 26(1), 81-90, 2018.
     [BibTex, sciendo(openaccess)] ]
6. 2017
   • Karol Pąk, The Matiyasevich Theorem. Preliminaries, Formalized Mathematics, 25(4), 315-325, 2017.
     [BibTex, sciendo(openaccess) ]
   • Marcin Acewicz, Karol Pąk, The Pell's Equation, Formalized Mathematics, 25(3), 197–204, 2017.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Artur Korniłowicz, Basel Problem, Formalized Mathematics, 25(2), 149-155, 2017.
     [BibTex, sciendo(openaccess)]
   • Artur Korniłowicz, Karol Pąk, Basel Problem - Preliminaries, Formalized Mathematics, 25(2), 141-147, 2017.
     [BibTex, sciendo(openaccess)]
   • Artur Korniłowicz, Karol Pąk, Vieta’s Formula about the Sum of Roots of Polynomial , Formalized Mathematics, 25(2), 87-92, 2017.
     [BibTex, sciendo(openaccess)]
7. 2016
   • Karol Pąk, Leibniz Series for π, Formalized Mathematics, 24(4), 275-280, 2016.
     [BibTex, sciendo(openaccess)]
8. 2015
   • Karol Pąk, Euler's Partition Theorem, Formalized Mathematics, 23(2), 93-99, 2015.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Flexary Operations, Formalized Mathematics, 23(2), 81-92, 2015.
     [BibTex, sciendo(openaccess)]
9. 2014
   • Karol Pąk, Topological Manifolds, Formalized Mathematics, 22(2), 179-186, 2014.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Bertrand’s Ballot Theorem, Formalized Mathematics, 22(2), 119-123, 2014.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Brouwer Invariance of Domain Theorem, Formalized Mathematics, 22(1), 21–28, 2014.
     [BibTex, sciendo(openaccess)]
   • Karol Pąk, Tietze Extension Theorem for n-dimensional spaces, Formalized Mathematics, 22(1), 11-19, 2014.
     [BibTex, sciendo(openaccess)]
10. 2012
    • Karol Pąk, The Friendship Theorem, Formalized Mathematics, 20(3), 235–237, 2012.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, The Rotation Group, Formalized Mathematics, 20(1), 23-29, 2012.
      [BibTex, sciendo(openaccess)]
11. 2011
    • Karol Pąk, Brouwer Fixed Point Theorem in the General Case, Formalized Mathematics, 19(3), 153–155, 2011.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Brouwer Fixed Point Theorem for Simplexes, Formalized Mathematics, 19(3), 2147–152, 2011.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Continuity of Barycentric Coordinates in Euclidean Topological Spaces, Formalized Mathematics, 19(3), 141–146, 2011.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Linear Transformations of Euclidean Topological Spaces. Part II, Formalized Mathematics, 19(2), 2109–112, 2011.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Linear Transformations of Euclidean Topological Spaces, Formalized Mathematics, 19(2), 103–108, 2011.
      [BibTex, sciendo(openaccess)]
12. 2010
    • Karol Pąk, Sperner’s Lemma, Formalized Mathematics, 18(4), 189-196, 2010.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, The Geometric Interior in Real Linear Spaces, Formalized Mathematics, 18(3), 185–188, 2010.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Abstract Simplicial Complexes, Formalized Mathematics, 18(1), 95–106, 2010.
      [BibTex, sciendo(openaccess)] [
    • Karol Pąk, Affine Indepedence in Vector Spaces, Formalized Mathematics, 18(1), 87–93, 2010.
      [BibTex, sciendo(openaccess)]
13. 2009
    • Karol Pąk, Small Inductive Dimension Of Topological Spaces Part II, Formalized Mathematics, 17(3), 219–222, 2009.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Small Inductive Dimension Of Topological Spaces, Formalized Mathematics, 17(3), 207–212, 2009.
      [BibTex,sciendo(openaccess)]
    • Karol Pąk, Basic Properties of Metrizable Topological Spaces, Formalized Mathematics, 17(3), 201–205, 2009.
      [BibTex, sciendo(openaccess)]
14. 2008
    • Karol Pąk, Jordan Matrix Decomposition, Formalized Mathematics, 16(4), 299–306, 2008.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Eigenvalues of a Linear Transformation, Formalized Mathematics, 16(4), 291–297, 2008.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Linear Map of Matrices, Formalized Mathematics, 16(3), 275–281, 2008.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Block Diagonal Matrices, Formalized Mathematics, 16(3), 1265–274, 2008.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Solutions of Linear Equations, Formalized Mathematics, 16(1), 81–92, 2008.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Complete Spaces, Formalized Mathematics, 16(1), 35–43, 2008.
      [BibTex, sciendo(openaccess)]
15. 2007
    • Karol Pąk, Basic Properties of the Rank of Matrices over a Field, Formalized Mathematics, 15(4), 199–211, 2007.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Andrzej Trybulec, Laplace Expansion, Formalized Mathematics, 15(3), 143–150, 2007.
      [BibTex, sciendo(openaccess)]
    • Karol Pąk, Basic Propeties of Determinants of Square Matrices over a Field, Formalized Mathematics, 15(1), 17-25, 2007.
      [BibTex, sciendo(openaccess)]
16. 2006
    • Karol Pąk, The Calatan Numbers. Part II, Formalized Mathematics, 14(4), 153-159, 2006.
      [BibTex, sciendo(openaccess)]
17. 2005
    • Karol Pąk, Cardinal Numbers and Finite Set, Formalized Mathematics, 13(3), 385-389, 2004.
      [BibTex, Publisher's site, PDF(openaccess)]
    • Karol Pąk, Stirling Numbers of the Second Kind, Formalized Mathematics, 13(2), 337-345, 2004.
      [BibTex, Publisher's site, PDF(openaccess)]
18. 2004
    • Karol Pąk, The Nagata-Smirnov Theorem. Part II, Formalized Mathematics, 12(3), 385-389, 2004.
      [BibTex, Publisher's site, PDF(openaccess)]
    • Karol Pąk, The Nagata-Smirnov Theorem. Part I, Formalized Mathematics, 12(3), 341-346, 2004.
      [BibTex, Publisher's site, PDF(openaccess)]

Others:

• Dominik Tomaszuk, Karol Pąk, Reducing vertices in property graphs Plos One, 13(2):1-25, 2018.
  [BibTex, Publisher's site, PDF(openaccess)]
• Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar Journal of Automated Reasoning, 2017.
  [BibTex, Publisher's site, PDF(openaccess)]
• Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban, Mizar: State-of-the-art and Beyond. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer, 2015.
  [BibTex, Publisher's site]
• Dominik Tomaszuk, Karol Pąk, Henryk Rybinski, Trust in RDF Graphs. In T. Morzy, T. Harder, and R. Wrembel, editors, Advances in Databases and Information Systems - 16th East European Conference, ADBIS 2012, Poznań, Poland, September 18-21, 2012. Proceedings II, volume 186 of Advances in Intelligent Systems and Computing, pages 273-283, Springer, 2012.
  [BibTex, Publisher's site]
• Bożena Piórkowska, Janusz Rafałko, Łukasz Kalinowski, Karol Pąk, Parts of Speech Recognition System for the Text-based, Polish Speech Synthesizer. In 11th International Conference on Speech and Computer (SPECOM 2006), St. Petersburg, 25-29 June 2006, pages 471-473, 2006.
  [BibTex, Publisher's site, PDF]