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.

theorem Imo1988Q6.constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop} (h₀ : H x y) (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop) (H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) (H_symm : ∀ {x y : ℕ}, H x y ↔ H y x) (H_zero : ∀ {x : ℕ}, H x 0 → claim) (H_diag : ∀ {x : ℕ}, H x x → claim) (H_desc : ∀ {x y : ℕ}, 0 < x → x < y → ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) (H_base : ∀ {x y : ℕ}, H x y → base x y → claim) : claim

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.

theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) : ∃ (d : ℕ), d ^ 2 = (a ^ 2 + b ^ 2) / (a * b + 1)

Question 6 of IMO1988. If a and b are two natural numbers such that a*b+1 divides a^2 + b^2, show that their quotient is a perfect square.