Scientific Visits:

• 4/2023 - 5/2023   one month; scientific visits; University of Innsbruck, Austria;
• 1/2020 - 1/2020   one week; scientific visits; University of Innsbruck, Austria;
• 10/2018 - 10/2018   one and a half week; scientific visits; University of Innsbruck, Austria; Technical University of Munic, Germany;
• 5/2018 - 5/2018   one week; scientific visits; Czech Technical University, Praga, Czech Republic.
• 11/2017 - 11/2017   two weeks; scientific visits; University of Innsbruck, Innsbruck, Austria.
• 11/2016 - 11/2016   one week;scientific visits; Czech Technical University, Praga, Czech Republic.
• 10/2016 - 10/2016   two weeks; scientific visits; University of Innsbruck, Innsbruck, Austria.
• 9/2015 - 9/2015   two weeks; scientific visits; University of Innsbruck, Innsbruck, Austria.
• 1/2007 - 3/2007   two months; scientific exchange; Shinshu University, Nagano, Japan.

Grants:

• 7/2016 - 7/2019   Isabelle Emulator for Mizar: Environment for Mizar Mathematical Library Reverificationa (DEC-2015/19/D/ST6/01473), granted by Polish National Science Center, project manager: Karol Pąk.
• 5/2016 - 4/2018   Independent Verification of Mizar Logic (PL 03/2016), granted by the OeAD Scientific & Technological Cooperation with Poland, poject coordinator at the Polish side: Karol Pąk.
• 7/2013 - 1/2017   Algorithms concerning the legibility of natural deduction proofs (DEC-2012/07/N/ST6/02147), granted by Polish National Science Center, project manager: Karol Pąk.
• 5/2009 - 5/2012   Management of a large repository of computer verified mathematical knowledge (N N519 385136), granted by Polish Ministry of Science and Higher Education, investigator, project manager: Andrzej Trybulec.

Membership in Academic Societies:

• Association of Mizar Users

100 Theorems:

List of solved formalization problems from the Formalizing 100 Theorems:

• 14. Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + ..... [BibTex, sciendo(openaccess)]
• 26. The Partition Theorem. [BibTex, sciendo(openaccess)]
• 30. The Ballot Problem. [BibTex, sciendo(openaccess)]
• 36. Brouwer Fixed Point Theorem. [BibTex, sciendo(openaccess)]
• 39. Solutions to Pell's Equation. [BibTex, sciendo(openaccess)]
• 45. The Partition Theorem. [BibTex, sciendo(openaccess)]
• 58. Formula for the Number of Combinations. [BibTex, Publisher's site, PDF(openaccess)]
• 83. The Friendship Theorem. [BibTex, sciendo(openaccess)]
• 96. Principle of Inclusion/Exclusion. [BibTex, Publisher's site, PDF(openaccess)]
• 97. Cramer's Rule. [BibTex, sciendo(openaccess)]