Related papers: A Lean formalization of Matiyasevi\v{c}'s Theorem

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…

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the…

We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory. Hilbert's Tenth Problem was answered negatively by Yuri Matiyasevich, who showed…

This paper initiates a novel research direction in the theory of Diophantine equations: define an appropriate version of the equation's size, order all polynomial Diophantine equations starting from the smallest ones, and then solve the…

In this paper, we find all the solutions of the Diophantine equation $P_\ell + P_m +P_n=2^a$, in nonnegative integer variables $(n,m,\ell, a)$ where $P_k$ is the $k$-th term of the Pell sequence $\{P_n\}_{n\ge 0}$ given by $P_0=0$, $P_1=1$…

Myasnikov, Ushakov, and Won introduced power circuits in 2012 to construct a polynomial-time algorithm for the word problem in the Baumslag group, which has a non-elementary Dehn function. Power circuits are computational structures that…

Let $n$ be a positive integer. The Diophantine equation $n(x_1+x_2+\dots +x_n)=x_1x_2\dots x_n$, $1 \le x_1\le x_2\le \dots \le x_n$ is called Erd\H{o}s's last equation. We prove that $x_n\to \infty $ as $n\to \infty$ and determine all…

We study connections between linear equations over various semigroups and recursively enumerable sets of positive integers. We give variants of the universal Diophantine representation of recursively enumerable sets of positive integers…

Let E_n={x_i=1, x_i+x_j=x_k, x_i \cdot x_j=x_k: i,j,k \in {1,...,n}}. If Matiyasevich's conjecture on single-fold Diophantine representations is true, then for every computable function f:N->N there is a positive integer m(f) such that for…

Yuri Matiyasevich's theorem states that the set of all Diophantine equations which have a solution in non-negative integers is not recursive. Craig Smory\'nski's theorem states that the set of all Diophantine equations which have at most…

Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once…

Let E_n={x_i=1, x_i+x_j=x_k, x_i \cdot x_j=x_k: i,j,k \in {1,...,n}}. If Matiyasevich's conjecture on finite-fold Diophantine representations is true, then for every computable function f:N->N there is a positive integer m(f) such that for…

In this paper we consider the Diophantine equation \begin{align*}b^k +\left(a+b\right)^k &+ \cdots + \left(a\left(x-1\right) + b\right)^k=\\ &=d^l + \left(c+d\right)^l + \cdots + \left(c\left(y-1\right) + d\right)^l, \end{align*} where…

The sufficient conditions for insolvability of the Diophantine equation $\sum_{i=1}^{m}x_i^{n}=bc^{n}$ ($n, m \geq 2$, $b, c\in \mathbb{N}$) in nonnegative integers are obtained for the case where the canonical decomposition of the number…

This paper explores multiple closely related themes: bounding the complexity of Diophantine equations over the integers and developing mathematical proofs in parallel with formal theorem provers. Hilbert's Tenth Problem (H10) asks about the…

Diophantine problems involving recurrence sequences have a long history and is an actively studied topic within number theory. In this paper, we connect to the field by considering the equation \begin{align*} B_mB_{m+d}\dots…

In this note we will analyze a diophantine equation raised by Michael Bennett in [1] that is pivotal in establishing that powers of five has few digits in its ternary expansion. We will show that the Diophantine equation…

The ABC conjecture implies many conjectures and theorems in number theory, including the celebrated Fermat's Last Theorem. Mason-Stothers Theorem is a function field analogue of the ABC conjecture that admits a much more elementary proof…

We treat the functions $\star^k:{\mathbf N}\rightarrow{\mathbf N}$ where $\star:x\mapsto \star x := x(x+1)$. The set $\{\star^k x+1: \{x,k\}\subseteq{\mathbf N}\}$ is pairwise coprime; so, the set ${\mathbf P}$ of primes is infinite. Our…

Based on the MRDP theorem, we introduce the ideas of the proof equation of a formula and universal proof equation of Peano Arithmetic (PA); and then, combining universal proof equation and G\"odel's Second Incompleteness Theorem, it is…