Pell's equation and Matiyasevic's theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file solves Pell's equation, i.e. integer solutions to
x ^ 2 - d * y ^ 2 = 1
in the special case that
d = a ^ 2 - 1.
This is then applied to prove Matiyasevic's theorem that the power
function is Diophantine, which is the last key ingredient in the solution to Hilbert's tenth
problem. For the definition of Diophantine function, see
For results on Pell's equation for arbitrary (positive, non-square)
Main definition #
pellis a function assigning to a natural number
n-th solution to Pell's equation constructed recursively from the initial solution
Main statements #
eq_pellshows that every solution to Pell's equation is recursively obtained using
matiyasevicshows that a certain system of Diophantine equations has a solution if and only if the first variable is the
x-component in a solution to Pell's equation - the key step towards Hilbert's tenth problem in Davis' version of Matiyasevic's theorem.
eq_pow_of_pellshows that the power function is Diophantine.
Implementation notes #
The proof of Matiyasevic's theorem doesn't follow Matiyasevic's original account of using Fibonacci numbers but instead Davis' variant of using solutions to Pell's equation.
- M. Carneiro, A Lean formalization of Matiyasevič's theorem
- M. Davis, Hilbert's tenth problem is unsolvable
Pell's equation, Matiyasevic's theorem, Hilbert's tenth problem
The Pell sequences, i.e. the sequence of integer solutions to
x ^ 2 - d * y ^ 2 = 1, where
d = a ^ 2 - 1, defined together in mutual recursion.