Diophantine functions and Matiyasevic's theorem #
Hilbert's tenth problem asked whether there exists an algorithm which for a given integer polynomial determines whether this polynomial has integer solutions. It was answered in the negative in 1970, the final step being completed by Matiyasevic who showed that the power function is Diophantine.
Here a function is called Diophantine if its graph is Diophantine as a set. A subset S ⊆ ℕ ^ α
in
turn is called Diophantine if there exists an integer polynomial on α ⊕ β
such that v ∈ S
iff
there exists t : ℕ^β
with p (v, t) = 0
.
Main definitions #
is_poly
: a predicate stating that a function is a multivariate integer polynomial.poly
: the type of multivariate integer polynomial functions.dioph
: a predicate stating that a setS ⊆ ℕ^α
is Diophantine, i.e. thatdioph_fn
: a predicate on a function stating that it is Diophantine in the sense that its graph is Diophantine as a set.
Main statements #
pell_dioph
states that solutions to Pell's equation form a Diophantine set.pow_dioph
states that the power function is Diophantine, a version of Matiyasevic's theorem.
References #
- M. Carneiro, A Lean formalization of Matiyasevic's theorem
- M. Davis, Hilbert's tenth problem is unsolvable
Tags #
Matiyasevic's theorem, Hilbert's tenth problem
TODO #
- Finish the solution of Hilbert's tenth problem.
- Connect
poly
tomv_polynomial
Equations
- decidable_list_all p l = decidable_of_decidable_of_iff (list.decidable_ball (λ (x : α), p x) l) _
- proj : ∀ {α : Sort u_1} (i : α), is_poly (λ (x : α → ℕ), ↑(x i))
- const : ∀ {α : Sort u_1} (n : ℤ), is_poly (λ (x : α → ℕ), n)
- sub : ∀ {α : Sort u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x - g x)
- mul : ∀ {α : Sort u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), (f x) * g x)
A predicate asserting that a function is a multivariate integer polynomial. (We are being a bit lazy here by allowing many representations for multiplication, rather than only allowing monomials and addition, but the definition is equivalent and this is easier to use.)
The constant function with value n : ℤ
.
Equations
- poly.const n = ⟨λ (x : α → ℕ), n, _⟩
Equations
- poly.has_zero = {zero := poly.zero α}
Equations
- poly.has_one = {one := poly.one α}
Equations
- poly.has_sub = {sub := poly.sub α}
Equations
- poly.has_neg = {neg := poly.neg α}
Equations
- poly.has_add = {add := poly.add α}
Equations
- poly.has_mul = {mul := poly.mul α}
Equations
- poly.comm_ring = {add := has_add.add poly.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add poly.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg poly.has_neg, sub := has_sub.sub poly.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := poly.neg α}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul poly.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul poly.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
The sum of squares of a list of polynomials. This is relevant for
Diophantine equations, because it means that a list of equations
can be encoded as a single equation: x = 0 ∧ y = 0 ∧ z = 0
is
equivalent to x^2 + y^2 + z^2 = 0
.
Equations
- poly.sumsq (p :: ps) = p * p + poly.sumsq ps
- poly.sumsq list.nil = 0
Map the index set of variables, replacing x_i
with x_(f i)
.
Functions from option
can be combined similarly to vector.cons
A version of Matiyasevic's theorem