<abstract xmlns="http://www.w3.org/1999/xhtml">

In our previous work [7] we prove that the set of prime numbers is diophantine using the 26-variable polynomial proposed in [4]. In this paper, we focus on the reduction of the number of variables to 10 and it is the smallest variables number known today [5], [10]. Using the Mizar [3], [2] system, we formalize the first step in this direction by proving Theorem 1 [5] formulated as follows: Let <italic>k</italic> ∈ ℕ. Then <italic>k</italic> is prime if and only if there exists <italic>f, i, j, m, u</italic> ∈ ℕ+, <italic>r, s, t</italic> ∈ ℕ unknowns such that 
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0020_eq_001.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><mtable columnalign="left"><mtr columnalign="left"><mtd columnalign="left"><mrow><mi>D</mi><mi>F</mi><mi>I</mi><mi> </mi><mtext>is</mtext><mi> </mi><mtext>square</mtext><mi> </mi><mi> </mi><mi> </mi><mo>∧</mo><mi> </mi><mrow><mo>(</mo><mrow><msup><mrow><mi>M</mi></mrow><mn>2</mn></msup><mo>-</mo><mn>1</mn></mrow><mo>)</mo></mrow><msup><mrow><mi>S</mi></mrow><mn>2</mn></msup><mo>+</mo><mn>1</mn><mi> </mi><mi> </mi><mtext>is</mtext><mi> </mi><mi> </mi><mtext>square</mtext><mi> </mi><mi> </mi><mo>∧</mo></mrow></mtd></mtr><mtr columnalign="left"><mtd columnalign="left"><mrow><mrow><mo>(</mo><mrow><msup><mrow><mrow><mrow><mo>(</mo><mrow><mi>M</mi><mi>U</mi></mrow><mo>)</mo></mrow></mrow></mrow><mn>2</mn></msup><mo>-</mo><mn>1</mn></mrow><mo>)</mo></mrow><msup><mrow><mi>T</mi></mrow><mn>2</mn></msup><mo>+</mo><mn>1</mn><mi> </mi><mi> </mi><mtext>is</mtext><mi> </mi><mi> </mi><mtext>square</mtext><mo>∧</mo></mrow></mtd></mtr><mtr columnalign="left"><mtd columnalign="left"><mrow><mrow><mo>(</mo><mrow><mn>4</mn><msup><mrow><mi>f</mi></mrow><mn>2</mn></msup><mo>-</mo><mn>1</mn></mrow><mo>)</mo></mrow><msup><mrow><mrow><mrow><mo>(</mo><mrow><mi>r</mi><mo>-</mo><mi>m</mi><mi>S</mi><mi>T</mi><mi>U</mi></mrow><mo>)</mo></mrow></mrow></mrow><mn>2</mn></msup><mo>+</mo><mn>4</mn><msup><mrow><mi>u</mi></mrow><mn>2</mn></msup><msup><mrow><mi>S</mi></mrow><mn>2</mn></msup><msup><mrow><mi>T</mi></mrow><mn>2</mn></msup><mo>&lt;</mo><mn>8</mn><mi>f</mi><mi>u</mi><mi>S</mi><mi>T</mi><mrow><mo>(</mo><mrow><mi>r</mi><mo>-</mo><mi>m</mi><mi>S</mi><mi>T</mi><mi>U</mi></mrow><mo>)</mo></mrow></mrow></mtd></mtr><mtr columnalign="left"><mtd columnalign="left"><mrow><mi>F</mi><mi>L</mi><mo>|</mo><mrow><mo>(</mo><mrow><mi>H</mi><mo>-</mo><mi>C</mi></mrow><mo>)</mo></mrow><mi>Z</mi><mo>+</mo><mi>F</mi><mrow><mo>(</mo><mrow><mi>f</mi><mo>+</mo><mn>1</mn></mrow><mo>)</mo></mrow><mi>Q</mi><mo>+</mo><mi>F</mi><mrow><mo>(</mo><mrow><mi>k</mi><mo>+</mo><mn>1</mn></mrow><mo>)</mo></mrow><mrow><mo>(</mo><mrow><mrow><mo>(</mo><mrow><msup><mrow><mi>W</mi></mrow><mn>2</mn></msup><mo>-</mo><mn>1</mn></mrow><mo>)</mo></mrow><mi>S</mi><mi>u</mi><mo>-</mo><msup><mrow><mi>W</mi></mrow><mn>2</mn></msup><msup><mrow><mi>u</mi></mrow><mn>2</mn></msup><mo>+</mo><mn>1</mn></mrow><mo>)</mo></mrow></mrow></mtd></mtr></mtable></mrow></math>
<tex-math>\matrix{ {DFI\,is\,square\,\,\,{\Lambda}\,\left( {{M^2} - 1} \right){S^2} + 1\,\,is\,\,square\,\,{\Lambda}} \hfill \cr {\left( {{{\left( {MU} \right)}^2} - 1} \right){T^2} + 1\,\,is\,\,square{\Lambda}} \hfill \cr {\left( {4{f^2} - 1} \right){{\left( {r - mSTU} \right)}^2} + 4{u^2}{S^2}{T^2} &lt; 8fuST\left( {r - mSTU} \right)} \hfill \cr {FL|\left( {H - C} \right)Z + F\left( {f + 1} \right)Q + F\left( {k + 1} \right)\left( {\left( {{W^2} - 1} \right)Su - {W^2}{u^2} + 1} \right)} \hfill \cr }</tex-math>
</alternatives>
</disp-formula>
where auxiliary variables <italic>A − I, L, M, S − W, Q</italic> ∈ ℤ are simply abbreviations defined as follows <italic>W</italic> = 100<italic>fk</italic>(<italic>k</italic> + 1), <italic>U</italic> = 100<italic>u</italic>3<italic>W</italic> 3 + 1, <italic>M</italic> = 100<italic>mUW</italic> + 1, <italic>S</italic> = (<italic>M −</italic>1)<italic>s</italic>+<italic>k</italic>+1, <italic>T</italic> = (<italic>MU −</italic>1)<italic>t</italic>+<italic>W −k</italic>+1, <italic>Q</italic> = 2<italic>MW −W</italic> 2<italic>−</italic>1, <italic>L</italic> = (<italic>k</italic>+1)<italic>Q</italic>, <italic>A</italic> = <italic>M</italic>(<italic>U</italic> +1), <italic>B</italic> = <italic>W</italic> +1, <italic>C</italic> = <italic>r</italic> +<italic>W</italic> +1, <italic>D</italic> = (<italic>A</italic>2 <italic>−</italic>1)<italic>C</italic>2 +1, <italic>E</italic> = 2<italic>iC</italic>2<italic>LD</italic>, <italic>F</italic> = (<italic>A</italic>2 <italic>−</italic>1)<italic>E</italic>2 +1, <italic>G</italic> = <italic>A</italic>+<italic>F</italic> (<italic>F −A</italic>), <italic>H</italic> = <italic>B</italic>+2(<italic>j −</italic>1)<italic>C</italic>, <italic>I</italic> = (<italic>G</italic>2 <italic>−</italic>1)<italic>H</italic>2 +1. It is easily see that (0.1) uses 8 unknowns explicitly along with five implicit one for each diophantine relationship: is square, inequality, and divisibility. Together with <italic>k</italic> this gives a total of 14 variables. This work has been partially presented in [8].
</abstract>

Prime Representing Polynomial with 10 Unknowns – Introduction. Part II

<abstract xmlns="http://www.w3.org/1999/xhtml">

In this article we formalize in Mizar [1], [2] the final step of our attempt to formally construct a prime representing polynomial with 10 variables proposed by Yuri Matiyasevich in [4].
The first part of the article includes many auxiliary lemmas related to multivariate polynomials. We start from the properties of monomials, among them their evaluation as well as the power function on polynomials to define the substitution for multivariate polynomials. For simplicity, we assume that a polynomial and substituted ones as <italic>i</italic>-th variable have the same number of variables. Then we study the number of variables that are used in given multivariate polynomials. By the used variable we mean a variable that is raised at least once to a non-zero power. We consider both adding unused variables and eliminating them.
The second part of the paper deals with the construction of the polynomial proposed by Yuri Matiyasevich. First, we introduce a diophantine polynomial over 4 variables that has roots in integers if and only if indicated variable is the square of a natural number, and another two is the square of an odd natural number. We modify the polynomial by adding two variables in such a way that the root additionally requires the divisibility of these added variables. Then we modify again the polynomial by adding two variables to also guarantee the nonnegativity condition of one of these variables. Finally, we combine the prime diophantine representation proved in [7] with the obtained polynomial constructing a prime representing polynomial with 10 variables. This work has been partially presented in [8] with the obtained polynomial constructing a prime representing polynomial with 10 variables in Theorem (85).
</abstract>

Prime Representing Polynomial with 10 Unknowns

<abstract xmlns="http://www.w3.org/1999/xhtml">

This is the second part of a two-part article formalizing existence and uniqueness of algebraic closures, using the Mizar [2], [1] formalism. Our proof follows Artin’s classical one as presented by Lang in [3]. In the first part we proved that for a given field <italic>F</italic> there exists a field extension <italic>E</italic> such that every non-constant polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] has a root in <italic>E</italic>. Artin’s proof applies Kronecker’s construction to each polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> simultaneously. To do so we needed the polynomial ring <italic>F</italic> [<italic>X</italic>1, <italic>X</italic>2, ...] with infinitely many variables, one for each polynomal <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic>. The desired field extension <italic>E</italic> then is <italic>F</italic> [<italic>X</italic>1, <italic>X</italic>2, …]<italic>\I</italic>, where <italic>I</italic> is a maximal ideal generated by all non-constant polynomials <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]. Note, that to show that <italic>I</italic> is maximal Zorn’s lemma has to be applied.
In this second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension <italic>A</italic> of <italic>F</italic>, in which every non-constant polynomial <italic>p</italic> ∈ <italic>A</italic>[<italic>X</italic>] has a root. The field of algebraic elements of <italic>A</italic> then is an algebraic closure of <italic>F</italic>. To prove uniqueness of algebraic closures, e.g. that two algebraic closures of <italic>F</italic> are isomorphic over <italic>F</italic>, the technique of extending monomorphisms is applied: a monomorphism <italic>F</italic> → <italic>A</italic>, where <italic>A</italic> is an algebraic closure of <italic>F</italic> can be extended to a monomorphism <italic>E</italic> → <italic>A</italic>, where <italic>E</italic> is any algebraic extension of <italic>F</italic>. In case that <italic>E</italic> is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.
</abstract>

Existence and Uniqueness of Algebraic Closures

<abstract xmlns="http://www.w3.org/1999/xhtml">

In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace <italic>S</italic> of a Hilbert space <italic>H</italic>, any vector can be represented by the sum of a vector in <italic>S</italic> and a vector orthogonal to <italic>S.</italic> The formalization of orthogonal complements of Hilbert spaces has been stored in the Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.
</abstract>

Formalization of Orthogonal Decomposition for Hilbert Spaces

AHEAD OF PRINT

Volume 31 (2023): Issue 1 (September 2023)

Volume 30 (2022): Issue 4 (December 2022)

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 (December 2012)

Volume 20 (2012): Issue 2 (December 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 (January 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 (January 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 (January 2008)

Volume 16 (2008): Issue 3 (January 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 (January 2007)

Volume 15 (2007): Issue 1 (January 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)

Formalized Mathematics

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in formal methods and computer-checked mathematics. Full-length original research articles in English. Archival issues available at the journal's home page fm.mizar.org/.   To build a uniform and extensible computer-checked repository of mathematical knowledge.  Reconstruction of mathematics based on mechanization of mathematical reasoning.  To check a wide range of mathematical theorems using a computer in an automatic fashion.  General mathematics: especially topology, lattice theory, functional analysis.  Applications: computer-aided verification of software and hardware, computer-aided teaching of mathematics.   Why subscribe and read   Pioneering source of high quality research in formalized and mechanically checked mathematics.  The oldest journal in the field, a medium for the publication of research reporting pioneering findings of broad mathematical significance that are likely to advance the direction and thinking of the field.  Long-term experience in publishing original articles on mechanizing mathematics and various aspects of automated reasoning, since 1990.   Why submit   Fair and constructive peer review by international experts in the field (three referees are designated for the assessment of each manuscript) - double-blind review process.  New publishing technology: articles automatically translated from a formal language into English and automatically typeset, available in both forms - electronic and printed.  Articles abstracted by online indexing services and databases.   Rejection Rate   59% of submitted articles.  The rejection percentage is described in detail in the following paper, pp.239-240: dx.doi.org/10.1007/978-3-540-73086-6_20 Archiving  Sciendo archives the contents of this journal in Portico - digital long-term preservation service of scholarly books, journals and collections.  Plagiarism Policy  The editorial board is participating in a growing community of Similarity Check System's users in order to ensure that the content published is original and trustworthy. Similarity Check is a medium that allows for comprehensive manuscripts screening, aimed to eliminate plagiarism and provide a high standard and quality peer-review process. Back Issues fm.mizar.org/   Other Files  Addenda 2008Formalized Mathematics Bibliography File.Formalized Mathematics External Bibliography File.  "In years: 2016-2017, the English version of Formalized Mathematics was financed under agreements 548/P-DUN/2016 and 548/1/P-DUN/2016 with the funds from the Polish Minister of Science and Higher Education for the dissemination of science." 