Recent publications:


  1. 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)]
  2. 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)]
  3. 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)]
  4. Cezary Kaliszyk, Karol Pąk, Semantics of Mizar as an Isabelle Object Logic, Journal of Automated Reasoning, 2018.
    [BibTex, Publisher's site, PDF(openaccess)]
  5. 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)]

Publications:


The Mizar System in the Isabelle Logical Framework:

Improving Legibility of Formal Proofs:

Described Formalizations:

Formalized Mathematics:

  1. 2021
  1. 2020
  1. 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)]
  1. 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)] ]
  2. 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)]
  3. 2016
  4. 2015
  5. 2014
  6. 2012
  7. 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)]
  8. 2010
  9. 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)]
  10. 2008
  11. 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)]
  12. 2006
  13. 2005
  14. 2004

Others: