Every Diophantine set over the naturals has an integer representation with only 11 unknowns and degree below an explicit but huge bound.
A Lean formalization of Matiyasevi\v{c}'s Theorem
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
In this paper, we present a formalization of Matiyasevi\v{c}'s theorem, which states that the power function is Diophantine, forming the last and hardest piece of the MRDP theorem of the unsolvability of Hilbert's 10th problem. The formalization is performed within the Lean theorem prover, and necessitated the development of a small number theory library, including in particular the solution to Pell's equation and properties of the Pell $x,y$ sequences.
fields
math.NT 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization
Every Diophantine set over the naturals has an integer representation with only 11 unknowns and degree below an explicit but huge bound.