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 set is Diophantine, i.e. a setS ⊆ ℕ^α
is Diophantine if there exists a polynomial onα ⊕ β
such thatv ∈ S
iff there existst : ℕ^β
withp (v, t) = 0
.dioph_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
Multivariate integer polynomials #
Note that this duplicates mv_polynomial
.
- proj : ∀ {α : Type u_1} (i : α), is_poly (λ (x : α → ℕ), ↑(x i))
- const : ∀ {α : Type u_1} (n : ℤ), is_poly (λ (x : α → ℕ), n)
- sub : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x - g x)
- mul : ∀ {α : Type 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 type of multivariate integer polynomials
Equations
- poly.fun_like = {coe := subtype.val (λ (f : (α → ℕ) → ℤ), is_poly f), coe_injective' := _}
Helper instance for when there are too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
The constant function with value n : ℤ
.
Equations
- poly.const n = ⟨λ (x : α → ℕ), n, _⟩
Equations
- poly.has_zero = {zero := poly.const 0}
Equations
- poly.has_one = {one := poly.const 1}
Equations
- poly.inhabited α = {default := 0}
Equations
- poly.add_comm_group = {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 := has_neg.neg poly.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Equations
- poly.add_group_with_one = {int_cast := poly.const α, add := add_comm_group.add poly.add_comm_group, add_assoc := _, zero := add_comm_group.zero poly.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul poly.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg poly.add_comm_group, sub := add_comm_group.sub poly.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul poly.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), poly.const ↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
Equations
- poly.comm_ring = {add := has_add.add poly.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul poly.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg poly.add_group_with_one, sub := add_group_with_one.sub poly.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul poly.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast poly.add_group_with_one, nat_cast := add_group_with_one.nat_cast poly.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul poly.has_mul, mul_assoc := _, 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
Diophantine sets #
A partial function is Diophantine if its graph is Diophantine.
Equations
- dioph.dioph_pfun f = dioph {v : option α → ℕ | f.graph (v ∘ option.some, v option.none)}
A function is Diophantine if its graph is Diophantine.
Equations
- dioph.dioph_fn f = dioph {v : option α → ℕ | f (v ∘ option.some) = v option.none}
A version of Matiyasevic's theorem