IMO problems

Stream: maths

[Kevin Buzzard]

(following on from the IMO2019 thread ): IMO 1988 Q6 has just gone viral at some school maths camp which is taking place at Imperial. It's a famous problem -- the one about if $a$ and $b$ are positive integers such that $ab+1$ divides $a^2+b^2$ then the ratio $\frac{a^2+b^2}{ab+1}$ must be a perfect square. The proof is not too hard if you know the trick, see e.g. Wikipedia but very tough otherwise (as is sometimes the case for IMO problems).

[Kevin Buzzard]

The guy running the camp is going to make a little video about it, and I've been asked to supply a Lean proof ASAP. I have a busy day :-/ but might get to it later if nobody else takes the bait. The proof is that if the ratio is k, a given fixed non-square, then considering the set of bad pairs (a,b) for which the ratio is k one can choose an element of the set with b<=a and a+b minimised, and then check check that a'=kb-a is a smaller counterexample.

[Kevin Buzzard]

It would be good to ultimately get a solution in Patrick's formatter

[Johan Commelin]

Here is a little start:

import data.rat.basic

@[simp] lemma int.square_zero {n : ℤ} : n^2 = 0 ↔ n = 0 :=
begin
  rw pow_two,
  split,
  { contrapose!, intro h,
    rcases lt_trichotomy n 0 with H|rfl|H,
    { apply ne_of_gt, exact mul_pos_of_neg_of_neg H H },
    { contradiction },
    { apply ne_of_gt, exact mul_pos H H } },
  { rintro rfl, simp },
end

lemma int.square_pos {n : ℤ} : n^2 > 0 ↔ n ≠ 0 :=
begin
  rw ←not_iff_not, push_neg,
  split,
  { rw ←int.square_zero, intro h, apply le_antisymm h, exact pow_two_nonneg n },
  { rintro rfl, simp [pow_two] }
end

variables {a b : ℤ} (h : a*b + 1 ∣ a^2 + b^2)
include h

lemma nz : a*b + 1 ≠ 0 :=
begin
  cases h with c h,
  contrapose! h,
  simp [h],
  rw [add_eq_zero_iff' (pow_two_nonneg _) (pow_two_nonneg _)],
  rw [int.square_zero, int.square_zero],
  rintro ⟨rfl, rfl⟩,
  simpa using h,
end

lemma q6_aux (a b : ℤ) (h : a*b + 1 ∣ a^2 + b^2) :
  ∃ k : ℤ, a^2 + b^2 = k^2 * (a*b + 1) :=
sorry

lemma q6 (a b : ℤ) (h : a*b + 1 ∣ a^2 + b^2) :
  ∃ q : ℚ, q^2 = (a^2 + b^2)/(a*b + 1) :=
begin
  cases q6_aux a b h with k hk,
  use k,
  rw_mod_cast hk, rw rat.mk_eq_div,
  simp,
  rw mul_div_cancel,
  norm_cast,
  simpa using nz h,
end

[Alex J. Best]

I also started, but may not finish :rolling_on_the_floor_laughing:

import data.nat.basic
import data.int.basic
import order.basic
import algebra.ring
import tactic.wlog
import tactic.omega
import tactic.tidy
import tactic.library_search

local attribute [instance, priority 0] classical.prop_decidable

theorem q6 (a b : ℕ) (h : ((a*b + 1) ∣ (a^2 + b^2))) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a*b + 1)  :=
begin
suffices : ∀ a b : ℕ, ∀ (h : ((a*b + 1) ∣ (a^2 + b^2))), ∃ k : ℕ , k^2 = (a^2 + b^2) / (a*b + 1), by exact this a b h,
clear h a b, -- forget about a b now
-- the set of possible counterexamples
let A : set (ℕ × ℕ) := { ab | (ab.1*ab.2 + 1) ∣ (ab.1^2 + ab.2^2) ∧ ¬ (∃ k : ℕ , k^2 = (ab.1^2 + ab.2^2) / (ab.1*ab.2 + 1)) },
suffices : A = ∅, begin
  intros a b h,
  by_contradiction not_exists,
  have ab_in_A : (⟨ a, b ⟩ : ℕ × ℕ) ∈ A := begin dsimp, split, exact h, exact not_exists, end,
  rw set.eq_empty_iff_forall_not_mem at this,
  have := this ⟨a, b⟩,
  contradiction,
end,
by_contradiction h,
let r : (ℕ × ℕ) → ℕ := λ ⟨a, b⟩, a + b,
let min_elem := well_founded.min (measure_wf r) A h,
let a := max min_elem.1 min_elem.2,
let b := min min_elem.1 min_elem.2,
have min_is_elem : min_elem ∈ A := well_founded.min_mem (measure_wf r) A h,
dsimp at min_is_elem,
have ab_mem : (a, b) ∈ A := begin
  dsimp,
  by_cases min_elem.1 ≤ min_elem.2,
  {
      have : a = min_elem.2 := if_pos h,
      rw this,
      have : b = min_elem.1 := if_pos h,
      rw this,
      simp at min_is_elem,
      simp [mul_comm,min_is_elem],
  },
  {
      have : a = min_elem.1 := if_neg h,
      rw this,
      have : b = min_elem.2 := if_neg h,
      rw this,
      exact min_is_elem,
  }
end,
let x := (a^2 + b^2) / (a*b + 1),
let newa := x*b - a,
have new_mem : (newa, b) ∈ A := begin
  simp [newa, x],
  split,
end,
have new_smaller : measure r (newa, b) (a, b) := begin sorry end,
have := well_founded.not_lt_min (measure_wf r) A h new_mem,

end

[Johan Commelin]

Ok, I missed the positivity condition.

[Johan Commelin]

@Kevin Buzzard What does "positive" mean on IMO problems?

[Johan Commelin]

≥ 0 or > 0?

[Kevin Buzzard]

0

[Kevin Buzzard]

rofl > 0

[Johan Commelin]

Great.

[Johan Commelin]

The strategy would be to use prod.lex_wf

[Johan Commelin]

And well_found.min

[Johan Commelin]

I don't have working Lean nearby, but I think this should be very straightforward.

[Johan Commelin]

It would be nice to formalise a theorem standard_vieta_jumping and standard_vieta_jumping_2

[Johan Commelin]

(The latter would take two arguments, instead of pairs.)

[Johan Commelin]

Hmmm, maybe I should shut up and code before doing any more talking.

[Alex J. Best]

Its still true if you just assume nonneg right? At least that's how I justified using nat to myself so id have less hypotheses floating around

[Floris van Doorn]

Did we have this part already?

import data.int.basic

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
  (h : x * x - b * x + c = 0) : ∃ y : α,
    y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
  have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
  use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end

[Johan Commelin]

That's nice!

[Alex J. Best]

Oh cool, here's where I'm up to, going to stop for a while so feel free to combine them and finish (if you want to) I think that missing piece is almost everything (except some sillyness?)

import data.nat.basic
import data.int.basic
import order.basic
import algebra.ring
import tactic.wlog
import tactic.interactive
import tactic.omega
import tactic.abel
import tactic.linarith
import tactic.tidy
import tactic.library_search

local attribute [instance, priority 0] classical.prop_decidable

lemma max_add_min (a b : ℤ) : max a b + min a b = a + b :=
begin
  by_cases a ≤ b,
  {
      have : min a b = a := if_pos h,
      rw this,
      have : max a b = b := if_pos h,
      rw [this, add_comm],
  },
  {
      have : min a b = b := if_neg h,
      rw this,
      have : max a b = a := if_neg h,
      rw this,
  }
end

lemma dumb_measure_fact {α : Type*} (r : α → ℕ) (a b c : α) (h : r a = r b) : measure r c a ↔ measure r c b :=
begin
change r c < r a ↔ r c < r b,
rwa ← h,
end

theorem q6 (a b : ℤ) (ha : a > 0) (hb : b > 0) (h : ((a*b + 1) ∣ (a^2 + b^2))) : ∃ k : ℤ, k^2 = (a^2 + b^2) / (a*b + 1)  :=
begin
suffices : ∀ a b : ℤ, ∀ ha : a > 0, ∀ hb : b > 0, ∀ h : ((a*b + 1) ∣ (a^2 + b^2)), ∃ k : ℤ, k^2 = (a^2 + b^2) / (a*b + 1), by exact this a b ha hb h,
clear h ha hb a b, -- forget about a b now
-- the set of possible counterexamples
let A : set (ℤ × ℤ) := { ab | (ab.1 > 0) ∧ (ab.2 > 0) ∧ ((ab.1*ab.2 + 1) ∣ (ab.1^2 + ab.2^2)) ∧ ¬ (∃ k : ℤ, k^2 = (ab.1^2 + ab.2^2) / (ab.1*ab.2 + 1)) },
suffices : A = ∅, begin
  intros a b ha hb h,
  by_contradiction not_exists,
  have ab_in_A : (⟨ a, b ⟩ : ℤ × ℤ) ∈ A := begin rw set.mem_set_of_eq, split, exact ha, split, exact hb, split, exact h, exact not_exists, end,
  rw set.eq_empty_iff_forall_not_mem at this,
  have := this ⟨a, b⟩,
  contradiction,
end,
by_contradiction h,
let r : (ℤ × ℤ) → ℕ := λ ⟨a, b⟩, int.nat_abs (a + b),
let min_elem := well_founded.min (measure_wf r) A h,
let a := max min_elem.1 min_elem.2,
let b := min min_elem.1 min_elem.2,
have min_is_elem : min_elem ∈ A := well_founded.min_mem (measure_wf r) A h,
dsimp at min_is_elem,
have ab_mem : (a, b) ∈ A := begin
  dsimp,
  by_cases min_elem.1 ≤ min_elem.2,
  {
      have : a = min_elem.2 := if_pos h,
      rw this,
      have : b = min_elem.1 := if_pos h,
      rw this,
      simp at min_is_elem,
      simp [mul_comm,min_is_elem],
  },
  {
      have : a = min_elem.1 := if_neg h,
      rw this,
      have : b = min_elem.2 := if_neg h,
      rw this,
      exact min_is_elem,
  }
end,
rcases ab_mem with ⟨ha, hb, h1, h2⟩,
dsimp at *,

let x := (a^2 + b^2) / (a*b + 1),
have a2b2_pos : 0 < a^2 + b^2 := add_pos (pow_pos ha 2) (pow_pos hb 2),
have abadd1_pos : 0 < a*b + 1 := add_pos (mul_pos ha hb) int.one_pos,
have x_pos : 0 < x := sorry,
let newa := x*b - a,
have newa_pos : 0 < newa := by sorry,
have new_mem : (newa, b) ∈ A := begin
  squeeze_simp [newa],
  have : x = (newa^2 + b^2) / (newa*b + 1) := begin
  simp [newa],
  ring,
  apply eq.symm,
  rw int.div_eq_iff_eq_mul_right _ _,
  ring,
  sorry,
  sorry,
  sorry,
  end,
  split,
  {
  ring,
  sorry,
  },
  {sorry,
  },
end,
have new_smaller : measure r (newa, b) (a, b) := begin
 suffices : ((int.nat_abs (newa + b)) : ℤ) < (int.nat_abs (a + b)),
 exact int.coe_nat_lt.mp this,
 rw (int.nat_abs_of_nonneg $ le_of_lt $ add_pos newa_pos hb),
 rw (int.nat_abs_of_nonneg $ le_of_lt $ add_pos ha hb),
 suffices : (newa < a),
 {linarith},
sorry
end,
have := well_founded.not_lt_min (measure_wf r) A h new_mem,
have measure_eq : r min_elem = r (a, b) := begin squeeze_simp [r, a, b], rw max_add_min,
sorry, end,
simp only [min_elem] at measure_eq,
rw dumb_measure_fact at this,
contradiction,
exact measure_eq,
end

[Kevin Buzzard]

Thanks to everyone for this. I am bogged down in a grant application and would never have got round to doing this over the next few days.

[Johan Commelin]

@Alex J. Best That's an impressively long proof!

[Alex J. Best]

Yeah thats my bad lol, I always forget to split things off into lemmas.

[Alex J. Best]

Also I still write things in an inefficient way I'm sure!

[Floris van Doorn]

I'm also working on this, and almost done. I'm struggling a bit with the argument (on the Wikipedia page) that x_2 is nonnegative: you have to show that x_2 * B + 1 != 0. If it were equal to 0, then you can easily derive a contradiction, using the fact that a ^ 2 + b ^ 2 = 0 -> a = b = 0. Is this fact already in mathlib?

import data.int.basic

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
  (h : x * x - b * x + c = 0) : ∃ y : α,
    y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
  have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
  use b - x, simp [left_distrib, mul_comm, this],
end

lemma fn_min_add_fn_max {α β} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β)
  (n m : α) : f (min n m) + f (max n m) = f n + f m :=
begin
  by_cases n ≤ m, { simp [h] },
  have : m ≤ n := le_of_lt (lt_of_not_ge h),
  simp [this]
end

lemma min_add_max {α} [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
  min n m + max n m = n + m :=
fn_min_add_fn_max id n m

lemma fn_min_mul_fn_max {α β} [decidable_linear_order α] [comm_semigroup β] (f : α → β)
  (n m : α) : f (min n m) * f (max n m) = f n * f m :=
begin
  by_cases n ≤ m, { simp [h] },
  have : m ≤ n := le_of_lt (lt_of_not_ge h),
  simp [this, mul_comm]
end

lemma min_mul_max {α} [decidable_linear_order α] [comm_semigroup α] (n m : α) :
  min n m * max n m = n * m :=
fn_min_mul_fn_max id n m

lemma min_le_max {α} [decidable_linear_order α] (n m : α) : min n m ≤ max n m :=
le_trans (min_le_left n m) (le_max_left n m)

lemma eq_iff_eq_of_eq {α} {x y z : α} (h : x = y) : x = z ↔ y = z :=
by rw [h]

theorem q6' (k : ℕ) (h : ∃ a b : ℕ, a * a + b * b = (a * b + 1) * k) : ∃ l : ℕ , l * l = k :=
begin
  have lemma1 : ∀{a b : ℤ}, a * a + b * b = (a * b + 1) * k ↔ b * b - (k * a) * b + (a * a - k) = 0,
  { intros a b, rw [right_distrib, ← sub_eq_iff_eq_add, ← sub_eq_zero],
    apply eq_iff_eq_of_eq, simp [mul_comm, mul_assoc] },
  cases nat.eq_zero_or_pos k with hk hk, { use 0, rw [hk], refl },
  let s : set (ℕ × ℕ) := { ab | ab.1 * ab.1 + ab.2 * ab.2 = (ab.1 * ab.2 + 1) * k },
  have hs : s ≠ ∅,
  { rw [set.ne_empty_iff_exists_mem], rcases h with ⟨a, b, hab⟩,
    use ⟨a, b⟩, simp [hab] },
  let r : ℕ × ℕ → ℕ := λ ab, ab.1 + ab.2,
  let s_min := well_founded.min (measure_wf r) s hs,
  let a' : ℕ := min s_min.1 s_min.2,
  let b' : ℕ := max s_min.1 s_min.2,
  let a : ℤ := a',
  let b : ℤ := b',
  have ha : 0 ≤ a := int.coe_zero_le a',
  have hb : 0 ≤ b := int.coe_zero_le b',
  have a_le_b : a ≤ b, { apply_mod_cast min_le_max },
  have hab : a * a + b * b = (a * b + 1) * k,
  { norm_cast,
    rw [fn_min_add_fn_max (λ x, x * x) s_min.1 s_min.2, min_mul_max s_min.1 s_min.2],
    exact well_founded.min_mem (measure_wf r) s hs },
  have h2ab : b * b - (k * a) * b + (a * a - k) = 0, { rwa [← lemma1] },
  rcases Vieta_formula_quadratic h2ab with ⟨c, h1c, h2c, h3c⟩,
  have h4c : c ≥ 0,
  { have : c * c + a * a = k * (c * a + 1),
    { sorry },
    have : (0 : ℤ) ≤ k * (c * a + 1),
    { rw [← this], apply add_nonneg; apply mul_self_nonneg },
    -- apply nonneg_of_mul_nonneg_right,
    sorry
     },
  have h5c : c < b,
  { apply lt_of_mul_lt_mul_left _ hb, rw [h3c],
    apply lt_of_lt_of_le (sub_lt_self _ _) (mul_le_mul a_le_b a_le_b ha hb),
    apply_mod_cast hk },
  obtain ⟨c', rfl⟩ : ∃ c' : ℕ, c = c',
  { use c.nat_abs, rw [int.nat_abs_of_nonneg h4c] },
  suffices : c' = 0,
  { subst this, use a', rw [int.coe_nat_zero, mul_zero, eq_comm, sub_eq_zero] at h3c,
    exact_mod_cast h3c },
  have hc' : (a', c') ∈ s,
  { rw [← lemma1] at h1c, exact_mod_cast h1c },
  have : a' + b' ≤ a' + c',
  { rw [← not_lt, min_add_max s_min.1 s_min.2],
    exact well_founded.not_lt_min (measure_wf r) s hs hc' },
  sorry
end


theorem q6 (a b : ℕ) (h : a*b + 1 ∣ a^2 + b^2) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a * b + 1)  :=
begin
  cases h with k hk,
  cases q6' k ⟨a, b, _⟩ with l hl,
  swap, rw [← nat.pow_two, ← nat.pow_two, hk],
  use l, rw [hk, nat.mul_div_cancel_left], rw [nat.pow_two, hl], apply nat.zero_lt_succ
end

[Chris Hughes]

I think nat.add_eq_zero and nat.mul_self_eq_zero are there.

[Kevin Buzzard]

In the proof that the complexes are a field it uses a lemma of the form x*x+y*y=0 -> x=0 but I can't remember the hypotheses, it might be totally ordered fields

[Floris van Doorn]

done!

import data.int.basic tactic.ring

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α} (h : x * x - b * x + c = 0) :
  ∃ y : α, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
  have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
  use b - x, simp [left_distrib, mul_comm, this],
end

lemma fn_min_add_fn_max {α β} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β)
  (n m : α) : f (min n m) + f (max n m) = f n + f m :=
begin
  by_cases n ≤ m, { simp [h] },
  have : m ≤ n := le_of_lt (lt_of_not_ge h),
  simp [this]
end

lemma min_add_max {α} [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
  min n m + max n m = n + m :=
fn_min_add_fn_max id n m

lemma fn_min_mul_fn_max {α β} [decidable_linear_order α] [comm_semigroup β] (f : α → β)
  (n m : α) : f (min n m) * f (max n m) = f n * f m :=
begin
  by_cases n ≤ m, { simp [h] },
  have : m ≤ n := le_of_lt (lt_of_not_ge h),
  simp [this, mul_comm]
end

lemma min_mul_max {α} [decidable_linear_order α] [comm_semigroup α] (n m : α) :
  min n m * max n m = n * m :=
fn_min_mul_fn_max id n m

lemma min_le_max {α} [decidable_linear_order α] (n m : α) : min n m ≤ max n m :=
le_trans (min_le_left n m) (le_max_left n m)

lemma eq_iff_eq_of_eq {α} {x y z : α} (h : x = y) : x = z ↔ y = z :=
by rw [h]

lemma mul_self_eq_zero {α} [domain α] {x : α} : x * x = 0 ↔ x = 0 :=
by simp

lemma mul_self_add_mul_self_eq_zero {α} [linear_ordered_ring α] {x y : α} :
  x * x + y * y = 0 ↔ x = 0 ∧ y = 0 :=
begin
  split; intro h, swap, { rcases h with ⟨rfl, rfl⟩, norm_num },
  have : y * y ≤ 0, { rw [← h], apply le_add_of_nonneg_left (mul_self_nonneg x) },
  have : y * y = 0 := le_antisymm this (mul_self_nonneg y),
  rw mul_self_eq_zero at this,
  have : x = 0, { rwa [this, mul_zero, add_zero, mul_self_eq_zero] at h },
  split; assumption
end

theorem q6' (k : ℕ) (h : ∃ a b : ℕ, a * a + b * b = (a * b + 1) * k) : ∃ l : ℕ , l * l = k :=
begin
  have lemma1 : ∀{a b : ℤ}, a * a + b * b = (a * b + 1) * k ↔ b * b - (k * a) * b + (a * a - k) = 0,
  { intros a b, rw [right_distrib, ← sub_eq_iff_eq_add, ← sub_eq_zero],
    apply eq_iff_eq_of_eq, simp [mul_comm, mul_assoc] },
  cases nat.eq_zero_or_pos k with hk hk, { use 0, rw [hk], refl },
  let s : set (ℕ × ℕ) := { ab | ab.1 * ab.1 + ab.2 * ab.2 = (ab.1 * ab.2 + 1) * k },
  have hs : s ≠ ∅,
  { rw [set.ne_empty_iff_exists_mem], rcases h with ⟨a, b, hab⟩,
    use ⟨a, b⟩, simp [hab] },
  let r : ℕ × ℕ → ℕ := λ ab, ab.1 + ab.2,
  let s_min := well_founded.min (measure_wf r) s hs,
  let a' : ℕ := min s_min.1 s_min.2,
  let b' : ℕ := max s_min.1 s_min.2,
  let a : ℤ := a',
  let b : ℤ := b',
  have ha : 0 ≤ a := int.coe_zero_le a',
  have hb : 0 ≤ b := int.coe_zero_le b',
  have a_le_b : a ≤ b, { apply_mod_cast min_le_max },
  have hab : a * a + b * b = (a * b + 1) * k,
  { norm_cast,
    rw [fn_min_add_fn_max (λ x, x * x) s_min.1 s_min.2, min_mul_max s_min.1 s_min.2],
    exact well_founded.min_mem (measure_wf r) s hs },
  have h2ab : b * b - (k * a) * b + (a * a - k) = 0, { rwa [← lemma1] },
  cases eq_or_lt_of_le ha with h2a h2a, -- if a = 0 it is easy
  { use b', rw [← h2a] at hab, have : b * b = k, { simpa using hab }, exact_mod_cast this },
  rcases Vieta_formula_quadratic h2ab with ⟨c, h1c, h2c, h3c⟩,
  have h4c : c ≥ 0,
  { have h1 : c * c + a * a = k * (c * a + 1),
    { rw [add_eq_zero_iff_eq_neg, sub_eq_iff_eq_add] at h1c, rw [h1c], ring },
    have : 0 ≤ ↑k * (c * a + 1),
    { rw [← h1], apply add_nonneg; apply mul_self_nonneg },
    have : 0 ≤ c * a + 1,
    { apply nonneg_of_mul_nonneg_left this, apply_mod_cast hk },
    have : 0 ≤ c * a,
    { apply int.le_of_lt_add_one, apply lt_of_le_of_ne this,
      intro h2, rw [← h2, mul_zero, mul_self_add_mul_self_eq_zero] at h1,
      exact ne_of_gt h2a h1.2 },
    apply nonneg_of_mul_nonneg_right this,
    exact h2a },
  have h5c : c < b,
  { apply lt_of_mul_lt_mul_left _ hb, rw [h3c],
    apply lt_of_lt_of_le (sub_lt_self _ _) (mul_le_mul a_le_b a_le_b ha hb),
    apply_mod_cast hk },
  obtain ⟨c', rfl⟩ : ∃ c' : ℕ, c = c',
  { use c.nat_abs, rw [int.nat_abs_of_nonneg h4c] },
  have hc' : (a', c') ∈ s,
  { rw [← lemma1] at h1c, exact_mod_cast h1c },
  have : a' + b' ≤ a' + c',
  { rw [← not_lt, min_add_max s_min.1 s_min.2],
    exact well_founded.not_lt_min (measure_wf r) s hs hc' },
  exfalso, apply not_le_of_lt h5c,
  apply_mod_cast le_of_add_le_add_left this
end

theorem q6 (a b : ℕ) (h : a*b + 1 ∣ a^2 + b^2) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a * b + 1)  :=
begin
  cases h with k hk,
  cases q6' k ⟨a, b, _⟩ with l hl,
  swap, rw [← nat.pow_two, ← nat.pow_two, hk],
  use l, rw [hk, nat.mul_div_cancel_left], rw [nat.pow_two, hl], apply nat.zero_lt_succ
end

[Floris van Doorn]

I used some of @Alex J. Best proof steps (involving finding the minimal pair).

[Alex J. Best]

I used some of Alex J. Best proof steps (involving finding the minimal pair).

Nice job! I'm glad some of what I did was helpful in the end :upside_down:

[Alex J. Best]

I wonder how much of the overall strategy can be made into a general infinite_descent or vieta_jumping theorem? For instance to prove the other example on the wikipedia page also:

Let a and b be positive integers such that ab divides a^2 + b^2 + 1. Prove that 3ab= a^2 + b^2 + 1

[Johan Commelin]

This is what I have so far:

import data.rat.basic
import tactic.linarith
import tactic.wlog

-- local attribute [instance] classical.prop_decidable
local attribute [simp] nat.pow_two

lemma nat.le_one_cases : ∀ n ≤ 1, n = 0 ∨ n = 1
| 0     h := by left;  refl
| 1     h := by right; refl
| (n+2) h := by linarith

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
  (h : x * x - b * x + c = 0) : ∃ y : α,
    y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
  have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
  use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end

lemma infinite_descent (P : ℕ → Prop) (n : ℕ) (hn : P n)
  (ih : ∀ n, n > 0 → P n → ∃ m < n, P m) : P 0 :=
begin
  -- let k := well_founded.min
  sorry
end

variables (k a b : ℕ)

@[reducible]
def P := a^2 + b^2 = k * a * b + k

variables {k a b}

lemma P_comm : P k a b ↔ P k b a :=
begin
  unfold P,
  rw [add_comm, mul_right_comm],
end

lemma P.symm (h : P k a b) : P k b a := P_comm.mp h

lemma P_of_eq (h : P k a a) : k ≤ 1 :=
begin
  replace h : 2 * a ^ 2 = k * (a ^ 2 + 1),
  { simpa [P, two_mul, mul_add, mul_assoc] using h, },
  contrapose! h,
  apply ne_of_lt,
  calc 2 * a^2 ≤ k * a^2       : nat.mul_le_mul_right _ h
           ... < k * (a^2 + 1) :
  begin
    apply mul_lt_mul',
    all_goals {linarith},
  end
end

lemma P.level_zero (h : P 0 a b) : a = 0 ∧ b = 0 :=
begin
  simpa [P] using h,
end

lemma P_zero (h : P k a 0) : k = a^2 :=
begin
  symmetry,
  simpa [P] using h
end

lemma P_quadratic_iff :
  P k a b ↔ (b:ℤ) * b - (k * a) * b + (a^2 - k) = 0 :=
begin
  unfold P,
  rw [← int.coe_nat_inj', ← sub_eq_zero],
  simp [pow_two],
end

lemma P.level_pos (h : P k a b) (H : a < b) : k > 0 :=
begin
  contrapose! H,
  rw nat.le_zero_iff at H,
  subst k,
  rcases h.level_zero with ⟨rfl, rfl⟩,
  refl
end

lemma P_root_ineq (h : P k a b) (H : a < b) : b ≤ k*a :=
begin
  rcases nat.exists_eq_add_of_le (le_of_lt H) with ⟨c, rfl⟩,
  rcases nat.exists_eq_add_of_lt (h.level_pos H) with ⟨l, rfl⟩,
  clear H,
  simp only [P, zero_add] at h ⊢,
  rw [nat.succ_mul, add_comm],
  apply add_le_add_right,
  simp at h,
  ring at h,
  -- contrapose! h,
end

lemma P_vieta_jump (h : P k a b) (H : a < b) : P k a (k*a - b) :=
begin
  have hb : b ≤ k*a := P_root_ineq h H,
  rw P_quadratic_iff at h ⊢,
  rcases Vieta_formula_quadratic h with ⟨c, h_root, hV₁, hV₂⟩,
  simpa only [eq_sub_of_add_eq' hV₁, int.coe_nat_sub hb] using h_root,
end

lemma level_square (h : P k a b) (H : k > 1) : ∃ d, k = d^2 :=
begin
  suffices h₀ : ∃ d, P k d 0,
  { rcases h₀ with ⟨d, hd⟩,
    use d,
    exact P_zero hd },
  apply infinite_descent (λ y, ∃ x, P k x y) b ⟨a, h⟩,
  clear h a b,
  rintros b bpos ⟨a, h⟩,
  have aneb : a ≠ b,
  { contrapose! H,
    subst H,
    exact P_of_eq h },
  rcases lt_trichotomy a b with h'|rfl|h',
  { use [a, H', k*a - b],
    rw P_comm,
    apply P_vieta_jump h H', },
  { specialize this (lt_trans bpos H') h.symm aneb.symm, }
end

[Johan Commelin]

This follows the ideas at the bottom of the Wiki page.

[Johan Commelin]

I've tried to write it in a style that is easy to document for use with Patrick's formatter.

[Johan Commelin]

I'm struggling with two the "wlog" part of the proof :expressionless:

[Johan Commelin]

Ok, here is my working solution

import data.rat.basic
import tactic.linarith
import tactic.wlog

local attribute [simp] nat.pow_two

lemma nat.le_one_cases : ∀ n ≤ 1, n = 0 ∨ n = 1
| 0     h := by left;  refl
| 1     h := by right; refl
| (n+2) h := by linarith

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
  (h : x * x - b * x + c = 0) : ∃ y : α,
    y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
  have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
  use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end

variables (k a b : ℕ)

@[reducible]
def P := a^2 + b^2 = k * a * b + k

variables {k a b}

lemma P_comm : P k a b ↔ P k b a :=
begin
  unfold P,
  rw [add_comm, mul_right_comm],
end

lemma P.symm (h : P k a b) : P k b a := P_comm.mp h

lemma level_le_one_of_eq (h : P k a a) : k ≤ 1 :=
begin
  replace h : 2 * a ^ 2 = k * (a ^ 2 + 1),
  { simpa [P, two_mul, mul_add, mul_assoc] using h, },
  contrapose! h,
  apply ne_of_lt,
  calc 2 * a^2 ≤ k * a^2       : nat.mul_le_mul_right _ h
           ... < k * (a^2 + 1) :
  begin
    apply mul_lt_mul',
    all_goals {linarith},
  end
end

lemma P.level_zero (h : P 0 a b) : a = 0 ∧ b = 0 :=
begin
  simpa [P] using h,
end

lemma P_zero (h : P k a 0) : k = a^2 :=
begin
  symmetry,
  simpa [P] using h
end

lemma P_quadratic_iff :
  P k a b ↔ (b:ℤ) * b - (k * a) * b + (a^2 - k) = 0 :=
begin
  unfold P,
  rw [← int.coe_nat_inj', ← sub_eq_zero],
  simp [pow_two],
end

lemma P.level_pos (h : P k a b) (H : a < b) : k > 0 :=
begin
  contrapose! H,
  rw nat.le_zero_iff at H,
  subst k,
  rcases h.level_zero with ⟨rfl, rfl⟩,
  refl
end

lemma P_vieta_jump (h : P k a b) (ha : a > 0) (H : a < b) :
  P k a (k*a - b) ∧ (k*a - b < a) :=
begin
  have hk := h.level_pos H,
  rw P_quadratic_iff at h ⊢,
  rcases Vieta_formula_quadratic h with ⟨c, h_root, hV₁, hV₂⟩,
  have hc := eq_sub_of_add_eq' hV₁,
  have hnat : c ≥ 0,
  { have Pkac : (a:ℤ)^2 + c^2 = (a * c + 1) * k,
    { rw [← sub_eq_zero, ← h_root],
      ring },
    have hpos : (a:ℤ)^2 + c^2 > 0,
    { apply add_pos_of_pos_of_nonneg,
      { rw pow_two,
        apply mul_pos;
        exact_mod_cast ha },
      { apply pow_two_nonneg } },
    rw Pkac at hpos,
    replace hpos : (a:ℤ) * c + 1 > 0 := pos_of_mul_pos_right hpos
      (by exact_mod_cast (le_of_lt hk)),
    replace hpos : (a:ℤ) * c ≥ 0 := int.le_of_lt_add_one hpos,
    apply nonneg_of_mul_nonneg_left hpos (by exact_mod_cast ha), },
  have b_le_ka : b ≤ k * a,
  { rw [← int.coe_nat_le, ← sub_nonneg],
    rw hc at hnat,
    exact_mod_cast hnat },
  have c_lt_a : c < a,
  { contrapose! hV₂,
    apply ne_of_gt,
    calc (b:ℤ) * c > a^2 :
      begin
        rw pow_two,
        apply mul_lt_mul,
        all_goals { linarith },
      end
      ... > a^2 - k : sub_lt_self _ (by exact_mod_cast hk) },
  subst c,
  split,
  { simpa only [int.coe_nat_sub b_le_ka] using h_root },
  { assumption_mod_cast },
end

lemma infinite_descent (P : ℕ → Prop) (n : ℕ) (hn : P n)
  (ih : ∀ n > 0, P n → (P 0 ∨ ∃ m < n, P m)) : P 0 :=
begin
  have h : P ≠ (∅ : set ℕ),
  { rintro rfl,
    assumption, },
  let k := well_founded.min nat.lt_wf P h,
  have hPk : P k := well_founded.min_mem nat.lt_wf P h,
  by_cases hk : k = 0,
  { rwa hk at hPk },
  replace hk : k > 0 := nat.pos_iff_ne_zero.mpr hk,
  rcases ih k hk hPk with H|⟨m,hm,hPm⟩,
  { assumption },
  { exfalso,
    exact well_founded.not_lt_min nat.lt_wf P h hPm hm, },
end

lemma level_square (h : P k a b) : ∃ d, k = d^2 :=
begin
  wlog : a ≤ b,
  swap,
  { exact this h.symm },
  by_cases H : a = b,
  { subst H,
    replace h := level_le_one_of_eq h,
    rcases nat.le_one_cases k h with rfl|rfl,
    { use 0,
      simp, },
    { use 1,
      simp, } },
  suffices h₀ : ∃ d, P k d 0,
  { rcases h₀ with ⟨d, hd⟩,
    use d,
    exact P_zero hd },
  replace H : a < b := lt_of_le_of_ne case H,
  { have := infinite_descent (λ y, ∃ x, P k x y ∧ (y > 0 → x < y)) b _ _,
    { simpa using this },
    { use [a, h],
      intro,
      assumption },
    { clear h H case a b,
      rintros b bpos ⟨a, h, h'⟩,
      specialize h' bpos,
      by_cases ha : a = 0,
      { left,
        subst a,
        simp,
        use [b, h.symm], },
      { right,
        use [a, h', k*a - b],
        replace ha : a > 0 := nat.pos_iff_ne_zero.mpr ha,
        cases P_vieta_jump h ha h',
        split,
        { rwa P_comm, },
        { intro,
          assumption } } } },
end

[Johan Commelin]

Maybe, strictly speaking, I should include a little wrapper at the end...

[Johan Commelin]

But Kevin didn't provide a formalisation. So I will say that I completed the problem (-;

[Johan Commelin]

@Kevin Buzzard Voila:

example {a b : ℕ} (h : a*b ∣ a^2 + b^2 + 1) :
  3*a*b = a^2 + b^2 + 1 :=
begin
  rcases h with ⟨k, hk⟩,
  suffices : k = 3, { simp * at *, ring, },
  simp only [nat.pow_two] at hk,
  apply constant_descent_vieta_jumping a b hk (λ x, k * x) (λ x, x*x + 1) (λ x y, x ≤ 1),
  { intros x y, simp, apply eq_iff_eq_cancel_left, ring },
  { intros x y, dsimp,
    rw [← int.coe_nat_inj', ← sub_eq_zero],
    apply eq_iff_eq_cancel_right,
    simp, ring, },
  { simp },
  { clear hk a b, intros x hx,
    have x_sq_dvd : x*x ∣ x*x*k := dvd_mul_right (x*x) k,
    rw ← hx at x_sq_dvd,
    simp only [nat.dvd_add_self_left, add_assoc] at x_sq_dvd,
    rcases x_sq_dvd with ⟨y, hy⟩,
    rw eq_comm at hy,
    simp [nat.mul_eq_one_iff] at hy,
    rcases hy with ⟨rfl,rfl⟩,
    simpa using hx.symm, },
  { clear hk a b,
    intros x y x_lt_y hx h_base h z h_root hV₁ hV₀,
    split,
    { have zy_pos : z * y ≥ 0,
      { rw hV₀, exact_mod_cast (nat.zero_le _) },
      apply nonneg_of_mul_nonneg_right zy_pos,
      linarith },
    { contrapose! hV₀,
      apply ne_of_gt,
      push_neg at h_base,
      calc z * y > x * y       : by apply mul_lt_mul_of_pos_right; linarith
             ... ≥ x * (x + 1) : by apply mul_le_mul; linarith
             ... > x * x + 1   :
        begin
          rw [mul_add, mul_one],
          apply add_lt_add_left,
          assumption_mod_cast
        end, } },
  { intros x y h h_base,
    rcases nat.le_one_cases x h_base with rfl|rfl,
    { simp at h, contradiction },
    { simp at h,
      have y_dvd : y ∣ y * k := dvd_mul_right y k,
      rw [← h, ← add_assoc, nat.dvd_add_left (dvd_mul_left y y)] at y_dvd,
      have y_eq : y = 1 ∨ y = 2 := nat.prime_two.2 y y_dvd,
      rcases y_eq with rfl|rfl,
      { simpa using h.symm, },
      { replace h : 2 * k = 2 * 3 := h.symm,
        apply nat.eq_of_mul_eq_mul_left _ h,
        exact (nat.succ_pos _), } } }
end

[Johan Commelin]

I'm quite satisfied with how this turned out

[Johan Commelin]

All the magic happens in apply constant_descent_vieta_jumping

[Johan Commelin]

Here's a gist with the full code: https://gist.github.com/jcommelin/619d66ccb3dcf534017051b0a1263f6f

[Johan Commelin]

I didn't try to golf, on purpose. I want to run this through Patrick's formatter now.

[Johan Commelin]

I hoped that omega would discharge some of the easier goals... but it didn't want to, see the other thread.