论文标题
正式对质数组的二磷剂表示
Formalizing a Diophantine Representation of the Set of Prime Numbers
论文作者
论文摘要
DPRM（Davis-Putnam-Robinson-Matiyasevich）定理是希尔伯特第10个问题负面解决方案的主要步骤。关于这个问题的工作将近三十年，导致了几个同样令人惊讶的结果。其中包括存在变量数量减少的二磷酸方程，以及代表特定集合的多项式的显式结构，特别是素数集。在这项工作中，我们在Mizar系统中正式化了这些结构。我们专注于使用10个变量的质数及其显式表示。这是当今已知的最小代表。为此，我们表明指数函数是二芬太汀，以及二项式系数和阶乘的相同特性。这种形式化是关于DPRM定理遵循二芬太丁的正式方法的下一步。
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.
