Volume 30 (2022): Issue 3 (October 2022)

Previous Mizar articles [7, 6, 5] formalized the implicit and inverse function theorems for Frechet continuously differentiable maps on Banach spaces. In this paper, using the Mizar system [1], [2], we formalize these theorems on Euclidean spaces by specializing them. We referred to [4], [12], [10], [11] in this formalization.

The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of unknowns in diophantine representations, using the Mizar [1], [2] formalism. The polynomial Jk(a1,…,ak,x)=∏ɛ1,…,ɛk∈{ ±1 }(x+ɛ1a1+ɛ2a2W)+…+ɛkakWk-1 {J_k}\left( {{a_1}, \ldots ,{a_k},x} \right) = \prod\limits_{{\varepsilon _1}, \ldots ,{\varepsilon _k} \in \left\{ { \pm 1} \right\}} {\left( {x + {\varepsilon _1}\sqrt {{a_1}} + {\varepsilon _2}\sqrt {{a_2}} W} \right) + \ldots + {\varepsilon _k}\sqrt {{a_k}} {W^{k - 1}}} with W=∑i=1kx i2 W = \sum\nolimits_{i = 1}^k {x_i^2} has integer coefficients and J_k(a₁, . . ., a_k, x) = 0 for some a₁, . . ., a_k, x ∈ ℤ if and only if a₁, . . ., a_k are all squares. However although it is nontrivial to observe that this expression is a polynomial, i.e., eliminating similar elements in the product of all combinations of signs we obtain an expression where every square root will occur with an even power. This work has been partially presented in [7].

This is the first part of a two-part article formalizing existence and uniqueness of algebraic closures using the Mizar system [1], [2]. Our proof follows Artin’s classical one as presented by Lang in [3]. In this first part we prove that for a given field F there exists a field extension E such that every non-constant polynomial p ∈ F [X] has a root in E. Artin’s proof applies Kronecker’s construction to each polynomial p ∈ F [X]\F simultaneously. To do so we need the polynomial ring F [X₁, X₂, ...] with infinitely many variables, one for each polynomal p ∈ F [X]\F . The desired field extension E then is F [X₁, X₂, ...]\I, where I is a maximal ideal generated by all non-constant polynomials p ∈ F [X]. Note, that to show that I is maximal Zorn’s lemma has to be applied.

In the second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension A of F, in which every non-constant polynomial p ∈ A[X] has a root. The field of algebraic elements of A then is an algebraic closure of F . To prove uniqueness of algebraic closures, e.g. that two algebraic closures of F are isomorphic over F, the technique of extending monomorphisms is applied: a monomorphism F → A, where A is an algebraic closure of F can be extended to a monomorphism E → A, where E is any algebraic extension of F . In case that E is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.

This is Erdős’s proof of the divergence of the sum of prime reciprocals, using the Mizar system [2], [3], as reported in “Proofs from THE BOOK” [1].

We formalize in the Mizar system [3], [4] some basic properties on left module over a ring such as constructing a module via a ring of endomorphism of an abelian group and the set of all homomorphisms of modules form a module [1] along with Ch. 2 set. 1 of [2].

The formalized items are shown in the below list with notations: M_ab for an Abelian group with a suffix “_ab” and M without a suffix is used for left modules over a ring.

1. The endomorphism ring of an abelian group denoted by End(M_ab).

2. A pair of an Abelian group M_ab and a ring homomorphism R→ρ R\mathop \to \limits^\rho End (M_ab) determines a left R-module, formalized as a function AbGrLMod(M_ab, ρ) in the article.

3. The set of all functions from M to N form R-module and denoted by Func_Mod_R(M, N).

4. The set R-module homomorphisms of M to N, denoted by Hom_R(M, N), forms R-module.

5. A formal proof of Hom_R(¯R, M) ≅M is given, where the ¯R denotes the regular representation of R, i.e. we regard R itself as a left R-module.

6. A formal proof of AbGrLMod(M′_ab, ρ′) ≅ M where M′_ab is an abelian group obtained by removing the scalar multiplication from M, and ρ′ is obtained by currying the scalar multiplication of M.

The removal of the multiplication from M has been done by the forgettable functor defined as AbGr in the article.

In this paper problems 17, 18, 26, 27, 28, and 98 from [9] are formalized, using the Mizar formalism [8], [2], [3], [6].

This paper reports on the formalization of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [5] using the Mizar system [4], [1], [2]. Problems 12, 13, 31, 32, 33, 35 and 40 belong to the chapter devoted to the divisibility of numbers, problem 47 concerns relatively prime numbers, whereas problems 76 and 79 are taken from the chapter on prime and composite numbers.

This paper reports on the formalization in Mizar system [1], [2] of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [7] (see [6] for details of this concrete dataset). This article is devoted mainly to arithmetic progressions: problems 52, 54, 55, 56, 60, 64, 70, 71, and 73 belong to the chapter “Arithmetic Progressions”, and problem 50 is from “Relatively Prime Numbers”.