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:

Improving Legibility of Formal Proofs:

Described Formalizations:

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
  3. 2020
  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
  8. 2015
  9. 2014
  10. 2012
  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
  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
  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
  17. 2005
  18. 2004

Others: