In this article, we define Diophantine sets using the Mizar formalism. We focus on selected properties of multivariate polynomials, i.e., functions of several variables to show finally that the class of Diophantine sets is closed with respect to the operations of union and intersection.
This article is the next in a series ,  aiming to formalize the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.
The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant , , . We analyze four equations from the Diophantine standpoint that are crucial in the bounded quantifier theorem, that is used in one of the approaches to solve the problem.
Based on our previous work , we prove that the value of a given binomial coefficient and factorial can be determined by its arguments in a Diophantine way. Then we prove that two products
where y > x are Diophantine.
The formalization follows , Z. Adamowicz, P. Zbierski  as well as M. Davis .
This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.
In our approach, we work with the Pell’s Equation defined in . We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form x2− (a2 − 1)y2 = 1  and its solutions considered as two sequences . We showed in  that the n-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation x = yi(a) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function y = xz is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product .
In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that every recursively enumerable set is Diophantine, where recursively enumerable sets have been defined by the Martin Davis normal form.
The formalization by means of Mizar system , ,  follows , Z. Adamowicz, P. Zbierski  as well as M. Davis .
In this article we prove the Euler’s Partition Theorem which states that the number of integer partitions with odd parts equals the number of partitions with distinct parts. The formalization follows H.S. Wilf’s lecture notes  (see also ).
Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ .
In this paper I present basic properties of block diagonal matrices over a set. In my approach the finite sequence of matrices in a block diagonal matrix is not restricted to square matrices. Moreover, the off-diagonal blocks need not be zero matrices, but also with another arbitrary fixed value.
In this article we formalize the Bertrand’s Ballot Theorem based on . Suppose that in an election we have two candidates: A that receives n votes and B that receives k votes, and additionally n ≥ k. Then this theorem states that the probability of the situation where A maintains more votes than B throughout the counting of the ballots is equal to (n − k)/(n + k).
This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
In this article we prove the Tietze extension theorem for an arbitrary convex compact subset of εn with a non-empty interior. This theorem states that, if T is a normal topological space, X is a closed subset of T, and A is a convex compact subset of εn with a non-empty interior, then a continuous function f : X → A can be extended to a continuous function g : T → εn. Additionally we show that a subset A is replaceable by an arbitrary subset of a topological space that is homeomorphic with a convex compact subset of En with a non-empty interior. This article is based on ;  and  can also serve as reference books.
In this article, we prove selected properties of Pell’s equation that are essential to finally prove the Diophantine property of two equations. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.
In this paper I present the Kronecker-Capelli theorem which states that a system of linear equations has a solution if and only if the rank of its coefficient matrix is equal to the rank of its augmented matrix.