# IMO 1988 Q6 and constant descent Vieta jumping #

Question 6 of IMO1988 is somewhat (in)famous. Several expert problem solvers could not tackle the question within the given time limit. The problem lead to the introduction of a new proof technique, so called “Vieta jumping”.

In this file we formalise constant descent Vieta jumping, and apply this to prove Q6 of IMO1988. To illustrate the technique, we also prove a similar result.

Constant descent Vieta jumping.

This proof technique allows one to prove an arbitrary proposition `claim`

,
by running a descent argument on a hyperbola `H`

in the first quadrant of the plane,
under the following conditions:

`h₀`

: There exists an integral point`(x,y)`

on the hyperbola`H`

.`H_symm`

: The hyperbola has a symmetry along the diagonal in the plane.`H_zero`

: If an integral point`(x,0)`

lies on the hyperbola`H`

, then`claim`

is true.`H_diag`

: If an integral point`(x,x)`

lies on the hyperbola`H`

, then`claim`

is true.`H_desc`

: If`(x,y)`

is an integral point on the hyperbola`H`

, with`x < y`

then there exists a “smaller” point on`H`

: a point`(x',y')`

with`x' < y' ≤ x`

.

For reasons of usability, the hyperbola `H`

is implemented as an arbitrary predicate.
(In question 6 of IMO1988, where this proof technique was first developed,
the predicate `claim`

would be `∃ (d : ℕ), d ^ 2 = k`

for some natural number `k`

,
and the predicate `H`

would be `fun a b ↦ a * a + b * b = (a * b + 1) * k`

.)

To ensure that the predicate `H`

actually describes a hyperbola,
the user must provide arguments `B`

and `C`

that are used as coefficients for a quadratic equation.
Finally, `H_quad`

is the proof obligation that the quadratic equation
`(y:ℤ) * y - B x * y + C x = 0`

describes the same hyperbola as the predicate `H`

.

For extra flexibility, one must provide a predicate `base`

on the integral points in the plane.
In the descent step `H_desc`

this will give the user the additional assumption that
the point `(x,y)`

does not lie in this base locus.
The user must provide a proof that the proposition `claim`

is true
if there exists an integral point `(x,y)`

on the hyperbola `H`

that lies in the base locus.
If such a base locus is not necessary, once can simply let it be `fun x y ↦ False`

.