Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2204.12311

Formalizing a Diophantine Representation of the Set of Prime Numbers

Karol Pąk·Cezary Kaliszyk
View original source ↗Read source document ↗Export metadata ↓

Abstract

The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert's 10th problem. Almost three decades of work on the problem have resulted in several equally surprising results. These include the existence of diophantine equations with a reduced number of variables, as well as the explicit construction of polynomials that represent specific sets, in particular the set of primes. In this work, we formalize these constructions in the Mizar system. We focus on the set of prime numbers and its explicit representation using 10 variables. It is the smallest representation known today. For this, we show that the exponential function is diophantine, together with the same properties for the binomial coefficient and factorial. This formalization is the next step in the research on formal approaches to diophantine sets following the DPRM theorem.

Explore related subjects

math.NTcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Karol Pąk, Cezary Kaliszyk. 2022-04-26. Formalizing a Diophantine Representation of the Set of Prime Numbers. https://arxiv.org/abs/2204.12311

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Asymptotic density of k-almost primes

Landau's well known asymptotic formula $$N_k(x):=\ \mid\{n\leq x : Ω(n)=k\}\mid \ \sim \left( \frac{x}{\log x} \right) \frac{(\log\log x)^{k-1}}{(k - 1)!}\ \ (x \rightarrow \infty),$$ which also holds for $$π_k(x):=\ \mid\{n\leq x : ω(n)=k\}\mid,$$ is known to be fairly poor for $k > 1$, and when $k$ is allowed to tend to infinity with $x$, the study of $N_k(x)$ and $π_k(x)$ becomes very technical [1, Chapter II.6, $§$ 6.1, p.200]. I hope to show that the method described below provides not only a more accurate approach, but rather increases in its asymptotic accuracy as $k$ tends to infinity.

math.NT↗
arXiv2026

Real quadratic base changes for $\mathrm{GL}_3$ and integral periods relations

We prove a $p$-adic divisibility between the automorphic periods of a cuspidal automorphic representation of $\mathrm{GL}_3(\mathbb{Q})$ and the periods of its Arthur-Clozel's base change to some real quadratic field $E$. This generalizes earlier works of Tilouine-Urban and of Hida in the case of classical modular forms. The divisibility we prove involves a new kind of automorphic periods, defined using the middle degree of the cuspidal cohomology of $\mathrm{GL}_3(E)$, instead of the top or bottom degrees. We also investigate the Rogawski's stable base change from the quasi-split unitary group $U_E$ associated with $E$ to $\mathrm{GL}_3(E)$. In this situation, we also obtain some results toward a $p$-adic divisibility of automorphic periods.

math.NT↗