Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/13661
Tytuł: | Prime Representing Polynomial |
Autorzy: | Pąk, Karol |
Słowa kluczowe: | prime number polynomial reduction diophantine equation |
Data wydania: | 2021 |
Data dodania: | 22-lip-2022 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 29, Issue 4, Pages 221-228 |
Abstrakt: | 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 MRDPtheorem [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)²+((g·k+g+k)·(h+j)+h−z)²+(2 · k³·(2·k+2)·(n + 1)²+1−f²)²+(p+q+z + 2·n−e)² + (e³·(e+ 2)·(a + 1)² + 1−o²)² + (x² −(a² −´1)·y² −1)² +(16 ·(a² − 1)· r²· y²· y² + 1 − u²)² + (((a + u²·(u² − a))² − 1)·(n + 4 · d · y)² +1 − (x + c · u)²)² +(m² − (a² −´1) · l² − 1)² + (k + i · (a − 1) − l)² + (n + l + v − y)² +(p + l · (a − n − 1) + b · (2 · a · (n + 1) − (n + 1)² − 1) − m)² +(q + y · (a − p − 1) + s · (2 · a · (p + 1) − (p + 1)² − 1) − x)² + (z + p · l · (a − p) +t · (2 · a · p − p² − 1) − p · m)² 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 N 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. |
Afiliacja: | Institute of Computer Science, University of Białystok, Poland |
URI: | http://hdl.handle.net/11320/13661 |
DOI: | 10.2478/forma-2021-0020 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-7099-1669 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2021 University of Białymstoku CC-BY-SA License ver. 3.0 or later |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2021, Volume 29, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2021-0020.pdf | 285,1 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL