| Publication | Date of Publication | Type |
|---|
| Prime representing polynomial with 10 unknowns -- introduction | 2024-04-22 | Paper |
| Combining higher-order logic with set theory formalizations | 2023-06-27 | Paper |
| Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | 2023-02-03 | Paper |
| Declarative Proof Translation (Short Paper) | 2023-02-03 | Paper |
| Prime representing polynomial | 2022-09-09 | Paper |
| Formalizing a Diophantine Representation of the Set of Prime Numbers | 2022-04-26 | Paper |
| Grothendieck universes | 2022-03-14 | Paper |
| AIM loops and the AIM conjecture | 2020-03-10 | Paper |
| A tale of two set theories | 2020-01-22 | Paper |
| Diophantine sets. II | 2019-11-19 | Paper |
| Formalization of the MRDP theorem in the Mizar system | 2019-11-19 | Paper |
| Semantics of Mizar as an Isabelle object logic | 2019-09-02 | Paper |
| Basic Diophantine relations | 2019-07-10 | Paper |
| Isabelle Formalization of Set Theoretic Structures and Set Comprehensions | 2019-03-14 | Paper |
| Isabelle import infrastructure for the Mizar Mathematical Library | 2018-10-18 | Paper |
| Diophantine sets. Preliminaries | 2018-10-17 | Paper |
| The Matiyasevich theorem. Preliminaries | 2018-10-16 | Paper |
| The role of the Mizar mathematical library for interactive proof development in Mizar | 2018-08-21 | Paper |
| Pell's equation | 2018-01-11 | Paper |
| Vieta's formula about the sum of roots of polynomials | 2017-10-06 | Paper |
| Basel problem -- preliminaries | 2017-10-06 | Paper |
| Basel problem | 2017-10-06 | Paper |
| Presentation and manipulation of Mizar properties in an Isabelle object logic | 2017-07-21 | Paper |
| Leibniz series for \(\pi\) | 2017-04-03 | Paper |
| Bertrand's ballot theorem | 2017-01-06 | Paper |
| Topological manifolds | 2017-01-06 | Paper |
| Improving legibility of formal proofs based on the close reference principle is NP-hard | 2016-05-26 | Paper |
| Readable Formalization of Euler’s Partition Theorem in Mizar | 2015-11-20 | Paper |
| Mizar: State-of-the-art and Beyond | 2015-11-20 | Paper |
| Flexary operations | 2015-08-19 | Paper |
| Euler's partition theorem | 2015-08-19 | Paper |
| Tietze extension theorem for \(n\)-dimensional spaces | 2014-11-05 | Paper |
| Brouwer invariance of domain theorem | 2014-11-05 | Paper |
| Improving legibility of natural deduction proofs is not trivial | 2014-09-30 | Paper |
| Automated Improving of Proof Legibility in the Mizar System | 2014-08-07 | Paper |
| Linear Transformations of Euclidean Topological Spaces | 2013-12-03 | Paper |
| Linear Transformations of Euclidean Topological Spaces. Part II | 2013-12-03 | Paper |
| Continuity of Barycentric Coordinates in Euclidean Topological Spaces | 2013-12-03 | Paper |
| Brouwer Fixed Point Theorem for Simplexes | 2013-12-03 | Paper |
| Brouwer Fixed Point Theorem in the General Case | 2013-12-03 | Paper |
| The Rotation Group | 2013-12-03 | Paper |
| The Friendship Theorem | 2013-10-08 | Paper |
| Methods of lemma extraction in natural deduction proofs | 2013-04-17 | Paper |
