- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English

#### Search

- Open Access

#### On Implicit and Inverse Function Theorems on Euclidean Spaces

Page range: 159 - 168

#### Abstract

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.

#### Keywords

- implicit function theorem
- inverse function theorem
- continuously differentiable function

#### MSC

- 26B10
- 47J07
- 68V20

- Open Access

#### Prime Representing Polynomial with 10 Unknowns – Introduction

Page range: 169 - 198

#### Abstract

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 _{k}_{1}, . . ., _{k}, x_{1}, . . ., _{k}, x_{1}, . . ., _{k }

#### Keywords

- polynomial reduction
- diophantine equation

#### MSC

- 11D45
- 68V20

- Open Access

#### Artin’s Theorem Towards the Existence of Algebraic Closures

Page range: 199 - 207

#### Abstract

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 _{1}, _{2}, ...] with infinitely many variables, one for each polynomal _{1}, _{2}, ...]

In the second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension

#### Keywords

- algebraic closures
- polynomial rings with countably infinite number of variables
- Emil Artin

#### MSC

- 12F05
- 68V20

- Open Access

#### The Divergence of the Sum of Prime Reciprocals

Page range: 209 - 210

#### Abstract

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].

#### Keywords

- primes
- asymptotics

#### MSC

- 11N05
- 11A41
- 68V20

- Open Access

#### Ring of Endomorphisms and Modules over a Ring

Page range: 211 - 221

#### Abstract

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: _{ab }_{ab}

1. The endomorphism ring of an abelian group denoted by _{ab}

2. A pair of an Abelian group _{ab }_{ab}_{ab}, ρ

3. The set of all functions from _{R}

4. The set _{R}

5. A formal proof of _{R}

6. A formal proof of _{ab}, ρ_{ab }

The removal of the multiplication from

#### Keywords

- module
- endomorphism ring

#### MSC

- 13C05
- 13C60
- 68V20

- Open Access

#### Elementary Number Theory Problems. Part IV

Page range: 223 - 228

#### Abstract

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

#### Keywords

- number theory
- divisibility
- primes

#### MSC

- 11A41
- 03B35
- 68V20

- Open Access

#### Elementary Number Theory Problems. Part V

Page range: 229 - 234

#### Abstract

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.

#### Keywords

- number theory
- divisibility
- primes

#### MSC

- 11A41
- 03B35
- 68V20

- Open Access

#### Elementary Number Theory Problems. Part VI

Page range: 235 - 244

#### Abstract

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”.

#### Keywords

- number theory
- arithmetic progression
- prime number

#### MSC

- 11B25
- 03B35
- 68V20