Issues

Journal & Issues

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

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (October 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

Volume 28 (2020): Issue 2 (July 2020)

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

Volume 27 (2019): Issue 2 (July 2019)

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

Volume 26 (2018): Issue 3 (October 2018)

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014)
Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

Volume 21 (2013): Issue 2 (June 2013)

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (September 2012)

Volume 20 (2012): Issue 2 (June 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (December 2011)

Volume 19 (2011): Issue 3 (September 2011)

Volume 19 (2011): Issue 2 (June 2011)

Volume 19 (2011): Issue 1 (March 2011)

Volume 18 (2010): Issue 4 (December 2010)

Volume 18 (2010): Issue 3 (September 2010)

Volume 18 (2010): Issue 2 (June 2010)

Volume 18 (2010): Issue 1 (March 2010)

Volume 17 (2009): Issue 4 (December 2009)

Volume 17 (2009): Issue 3 (September 2009)

Volume 17 (2009): Issue 2 (June 2009)

Volume 17 (2009): Issue 1 (March 2009)

Volume 16 (2008): Issue 4 (December 2008)

Volume 16 (2008): Issue 3 (September 2008)

Volume 16 (2008): Issue 2 (June 2008)

Volume 16 (2008): Issue 1 (March 2008)

Volume 15 (2007): Issue 4 (December 2007)

Volume 15 (2007): Issue 3 (September 2007)

Volume 15 (2007): Issue 2 (June 2007)

Volume 15 (2007): Issue 1 (March 2007)

Volume 14 (2006): Issue 4 (December 2006)

Volume 14 (2006): Issue 3 (September 2006)

Volume 14 (2006): Issue 2 (June 2006)

Volume 14 (2006): Issue 1 (March 2006)

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

Search

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

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

Search

8 Articles
Open Access

On Implicit and Inverse Function Theorems on Euclidean Spaces

Published Online: 30 Dec 2022
Page range: 159 - 168

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 169 - 198

Abstract

Summary

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 Jk(a1, . . ., ak, x) = 0 for some a1, . . ., ak, x ∈ ℤ if and only if a1, . . ., ak 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].

Keywords

  • polynomial reduction
  • diophantine equation

MSC

  • 11D45
  • 68V20
Open Access

Artin’s Theorem Towards the Existence of Algebraic Closures

Published Online: 30 Dec 2022
Page range: 199 - 207

Abstract

Summary

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 pF [X] has a root in E. Artin’s proof applies Kronecker’s construction to each polynomial pF [X]\F simultaneously. To do so we need the polynomial ring F [X1, X2, ...] with infinitely many variables, one for each polynomal pF [X]\F . The desired field extension E then is F [X1, X2, ...]\I, where I is a maximal ideal generated by all non-constant polynomials pF [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 pA[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 FA, where A is an algebraic closure of F can be extended to a monomorphism EA, 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.

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

Published Online: 30 Dec 2022
Page range: 209 - 210

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 211 - 221

Abstract

Summary

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: Mab 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(Mab).

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

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

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

5. A formal proof of HomRR, 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(Mab, ρ′) ≅ M where Mab 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.

Keywords

  • module
  • endomorphism ring

MSC

  • 13C05
  • 13C60
  • 68V20
Open Access

Elementary Number Theory Problems. Part IV

Published Online: 30 Dec 2022
Page range: 223 - 228

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 229 - 234

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 235 - 244

Abstract

Summary

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
8 Articles
Open Access

On Implicit and Inverse Function Theorems on Euclidean Spaces

Published Online: 30 Dec 2022
Page range: 159 - 168

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 169 - 198

Abstract

Summary

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 Jk(a1, . . ., ak, x) = 0 for some a1, . . ., ak, x ∈ ℤ if and only if a1, . . ., ak 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].

Keywords

  • polynomial reduction
  • diophantine equation

MSC

  • 11D45
  • 68V20
Open Access

Artin’s Theorem Towards the Existence of Algebraic Closures

Published Online: 30 Dec 2022
Page range: 199 - 207

Abstract

Summary

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 pF [X] has a root in E. Artin’s proof applies Kronecker’s construction to each polynomial pF [X]\F simultaneously. To do so we need the polynomial ring F [X1, X2, ...] with infinitely many variables, one for each polynomal pF [X]\F . The desired field extension E then is F [X1, X2, ...]\I, where I is a maximal ideal generated by all non-constant polynomials pF [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 pA[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 FA, where A is an algebraic closure of F can be extended to a monomorphism EA, 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.

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

Published Online: 30 Dec 2022
Page range: 209 - 210

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 211 - 221

Abstract

Summary

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: Mab 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(Mab).

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

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

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

5. A formal proof of HomRR, 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(Mab, ρ′) ≅ M where Mab 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.

Keywords

  • module
  • endomorphism ring

MSC

  • 13C05
  • 13C60
  • 68V20
Open Access

Elementary Number Theory Problems. Part IV

Published Online: 30 Dec 2022
Page range: 223 - 228

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 229 - 234

Abstract

Summary

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

Published Online: 30 Dec 2022
Page range: 235 - 244

Abstract

Summary

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

Plan your remote conference with Sciendo