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

The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this problem, using the Mizar system [1], [2], in two independent ways, proving the existence of a polynomial without formulating it explicitly as well as with its indication.
First, we reuse nearly all the techniques invented to prove the MRDP-theorem [11]. Applying a trick with Mizar schemes that go beyond first-order logic we give a short sophisticated proof for the existence of such a polynomial but without formulating it explicitly. Then we formulate the polynomial proposed in [6] that has 26 variables in the Mizar language as follows (<italic>w</italic>·<italic>z</italic>+<italic>h</italic>+<italic>j</italic>−<italic>q</italic>)2+((<italic>g</italic>·<italic>k</italic>+<italic>g</italic>+<italic>k</italic>)·(<italic>h</italic>+<italic>j</italic>)+<italic>h</italic>−<italic>z</italic>)2+(2 · <italic>k</italic>3·(2·<italic>k</italic>+2)·(<italic>n</italic> + 1)2+1−<italic>f</italic>2)2+ (<italic>p</italic> + <italic>q</italic> + <italic>z</italic> + 2 · <italic>n</italic> − <italic>e</italic>)2 + (<italic>e</italic>3 · (<italic>e</italic> + 2) · (<italic>a</italic> + 1)2 + 1 − <italic>o</italic>2)2 + (<italic>x</italic>2 − (<italic>a</italic>2 −′ 1) · <italic>y</italic>2 − 1)2 + (16 · (<italic>a</italic>2 − 1) · <italic>r</italic>2 · <italic>y</italic>2 · <italic>y</italic>2 + 1 − <italic>u</italic>2)2 + (((<italic>a</italic> + <italic>u</italic>2 · (<italic>u</italic>2 − <italic>a</italic>))2 − 1) · (<italic>n</italic> + 4 · <italic>d</italic> · <italic>y</italic>)2 + 1 − (<italic>x</italic> + <italic>c</italic> · <italic>u</italic>)2)2 + (<italic>m</italic>2 − (<italic>a</italic>2 −′ 1) · <italic>l</italic>2 − 1)2 + (<italic>k</italic> + <italic>i</italic> · (<italic>a</italic> − 1) − <italic>l</italic>)2 + (<italic>n</italic> + <italic>l</italic> + <italic>v</italic> − <italic>y</italic>)2 + (<italic>p</italic> + <italic>l</italic> · (<italic>a</italic> − <italic>n</italic> − 1) + <italic>b</italic> · (2 · <italic>a</italic> · (<italic>n</italic> + 1) − (<italic>n</italic> + 1)2 − 1) − <italic>m</italic>)2 + (<italic>q</italic> + <italic>y</italic> · (<italic>a</italic> − <italic>p</italic> − 1) + <italic>s</italic> · (2 · <italic>a</italic> · (<italic>p</italic> + 1) − (<italic>p</italic> + 1)2 − 1) − <italic>x</italic>)2 + (<italic>z</italic> + <italic>p</italic> · <italic>l</italic> · (<italic>a</italic> − <italic>p</italic>) + <italic>t</italic> · (2 · <italic>a</italic> · <italic>p</italic> − <italic>p</italic>2 − 1) − <italic>p</italic> · <italic>m</italic>)2 and we prove that that for any positive integer <italic>k</italic> so that <italic>k</italic> + 1 is prime it is necessary and sufficient that there exist other natural variables <italic>a</italic>-<italic>z</italic> for which the polynomial equals zero. 26 variables is not the best known result in relation to the set of prime numbers, since any diophantine equation over ℕ can be reduced to one in 13 unknowns [8] or even less [5], [13]. The best currently known result for all prime numbers, where the polynomial is explicitly constructed is 10 [7] or even 7 in the case of Fermat as well as Mersenne prime number [4]. We are currently focusing our formalization efforts in this direction.
</abstract>

The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this problem, using the Mizar system [1], [2], in two independent ways, proving the existence of a polynomial without formulating it explicitly as well as with its indication.
First, we reuse nearly all the techniques invented to prove the MRDP-theorem [11]. Applying a trick with Mizar schemes that go beyond first-order logic we give a short sophisticated proof for the existence of such a polynomial but without formulating it explicitly. Then we formulate the polynomial proposed in [6] that has 26 variables in the Mizar language as follows (w·z+h+j−q)2+((g·k+g+k)·(h+j)+h−z)2+(2 · k3·(2·k+2)·(n + 1)2+1−f2)2+ (p + q + z + 2 · n − e)2 + (e3 · (e + 2) · (a + 1)2 + 1 − o2)2 + (x2 − (a2 −′ 1) · y2 − 1)2 + (16 · (a2 − 1) · r2 · y2 · y2 + 1 − u2)2 + (((a + u2 · (u2 − a))2 − 1) · (n + 4 · d · y)2 + 1 − (x + c · u)2)2 + (m2 − (a2 −′ 1) · l2 − 1)2 + (k + i · (a − 1) − l)2 + (n + l + v − y)2 + (p + l · (a − n − 1) + b · (2 · a · (n + 1) − (n + 1)2 − 1) − m)2 + (q + y · (a − p − 1) + s · (2 · a · (p + 1) − (p + 1)2 − 1) − x)2 + (z + p · l · (a − p) + t · (2 · a · p − p2 − 1) − p · m)2 and we prove that that for any positive integer k so that k + 1 is prime it is necessary and sufficient that there exist other natural variables a-z for which the polynomial equals zero. 26 variables is not the best known result in relation to the set of prime numbers, since any diophantine equation over ℕ can be reduced to one in 13 unknowns [8] or even less [5], [13]. The best currently known result for all prime numbers, where the polynomial is explicitly constructed is 10 [7] or even 7 in the case of Fermat as well as Mersenne prime number [4]. We are currently focusing our formalization efforts in this direction.

Prime Representing Polynomial

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Prime Representing Polynomial"}

The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this...

Prime Representing Polynomial

Publié en ligne: 09 juil. 2022

Pages: 221 - 228

Accepté: 30 nov. 2021

DOI: https://doi.org/10.2478/forma-2021-0020

Mots clés
prime number, polynomial reduction, diophantine equation

© 2022 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Prime Representing Polynomial

Publié en ligne: 09 juil. 2022

Pages: 221 - 228

Accepté: 30 nov. 2021

DOI: https://doi.org/10.2478/forma-2021-0020

Mots clésprime number, polynomial reduction, diophantine equation

© 2022 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Mots clés
prime number, polynomial reduction, diophantine equation