## Stream: maths

### Topic: cheap IMO problem

#### Kevin Buzzard (Sep 25 2020 at 16:16):

IMO 1979 Q1:

 Let m and n be positive integers such that:

m/n = 1 - 1/2 + 1/3 - 1/4 + ... - 1/1318 + 1/1319.

Prove that m is divisible by 1979.


SPOILER ALERT LINK IMO 1979 Q1 solution should be easy to formalise now we have p-adic valuation, right?

import tactic

import algebra.big_operators.basic

open_locale big_operators

def h : fin 1320 → ℚ := λ n, (-1)^((n : ℕ)+ 1)/n

open nat

instance foo : fact (prime 1979) := by norm_num

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x, h x
→ 1979 ∣ p :=
begin
sorry
end


They were chatting about it on the IMO stream.

#### Kevin Buzzard (Sep 25 2020 at 16:18):

There's probably a better way to state it.

#### Kevin Buzzard (Sep 25 2020 at 16:28):

import tactic

import algebra.big_operators.basic

open_locale big_operators

open nat

instance foo : fact (prime 1979) := by norm_num

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
sorry
end


is nicer.

#### Kevin Buzzard (Sep 25 2020 at 20:01):

I made a start but now I have to eat:

import tactic

import algebra.big_operators.ring

import data.nat.parity

open_locale big_operators

open finset

open nat

instance foo : fact (prime 1979) := by norm_num

open finset

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
let a : ℚ := ∑ n in range 1320, (-1)^(n + 1) / n,
let b : ℚ := ∑ n in range 1320, 1 / n,
-- b - a = 2(1/2+1/4+...+1318)
-- = 1+1/2+1/3+...+1/659
let c : ℚ := ∑ n in range 660, 1 / n,
-- want b - a = c i.e. to formalise lines above
let e : ℕ ↪ ℕ := ⟨λ n, 2 * n, λ a b, mul_left_cancel' (by norm_num)⟩,
have h1 := sum_map (range 660) e (λ n, (1 : ℚ) / n),
-- first goal b - a = c,
-- hence a = sum from 660 to 1319
-- then they cancel
have h0 : b - a = c,
calc b - a = ∑ n in range 1320, (1/n - (-1)^(n+1)/n) : by rw sum_sub_distrib
... = ∑ n in range 1320, ite (even n) (2/n) 0 : by {
apply sum_congr rfl,
rintros x hx,
split_ifs,
{ rcases h with ⟨n, rfl⟩,
rw [pow_mul, pow_two],
simp, norm_num },
{ rw not_even_iff at h,
have h8 := nat.mod_add_div x 2,
rw h at h8,
suffices : (1 : ℚ) + (-1)^x = 0,
rw this, simp,
rw ← h8,
}
}
... = ∑ (x : ℕ) in filter even (range 1320), 2 / x : by rw sum_filter
... = ∑ (x : ℕ) in map e (range 660), (2 : ℚ) / x : by {
apply sum_congr, swap, simp,
apply finset.subset.antisymm,
sorry,
sorry
}
... = c : sorry,
sorry
end


#### Yakov Pechersky (Sep 27 2020 at 07:43):

Here's my fin powered attempt, I'm now struggling with collapsing the "telescoping" sum.

import tactic.ring_exp
import data.matrix.notation
import data.rat.cast

open_locale big_operators

def h {n : ℕ} : fin n → ℚ := λ k, (-1)^((k : ℕ)+ 1)/k

instance foo : fact (nat.prime 1979) := by norm_num

@[simp] lemma fin.coe_sub {n : ℕ} (x y : fin n) : (((x - y) : fin n) : ℕ) = (x : ℕ) - y :=
by { cases x, cases y, refl }

lemma fin.coe_bit0 {n : ℕ} {x : fin n} (h : (bit0 x : ℕ) < n) : ((bit0 x : fin n) : ℕ) = bit0 x :=
by { cases x, exact nat.mod_eq_of_lt h }

lemma fin.coe_bit1 {n : ℕ} {x : fin (n + 2)} (h : (bit1 x : ℕ) < n + 2) :
((bit1 x : fin (n + 2)) : ℕ) = bit1 x :=
begin
rw bit1 at h,
fin.coe_bit0 (lt_of_le_of_lt (nat.le_add_right _ _) h)] using nat.mod_eq_of_lt h,
end

section hF

variables {n : ℕ} (N : ℕ) (x : fin n)

def hF : ℚ := 1 / ((N + (x : ℕ)) : ℚ)

lemma shift : hF N.succ x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma reduce : @hF n.succ N x.cast_succ = @hF n N x :=
by simp [hF]

lemma hreduce : h x.cast_succ.cast_succ = h x :=
by simp [h]

lemma h_to_hF : (∑ x : fin (N * 2), h x) = ∑ x : fin N, hF N x :=
begin
induction N with N hN,
{ refl },
symmetry,
rw fin.sum_univ_cast_succ,
simp_rw shift N,
simp_rw reduce,
symmetry,
rw [nat.succ_mul, fin.sum_univ_cast_succ, fin.sum_univ_cast_succ],
simp_rw hreduce,
congr' 1,
congr,
{ have nh : (-1 : ℚ) ^ (N * 2 + 1) = -1,
{ rw [mul_comm],
have : (N : ℚ)⁻¹ = 2 / (N * 2),
{ norm_num [←one_div, mul_comm, div_mul_eq_div_mul_one_div] },
norm_num [h, hF, nh, this],
ring_exp },
{ have nh : (-1 : ℚ) ^ (N * 2 + 1 + 1) = 1,
{ rw [mul_comm],
norm_num [h, hF, nh],
ring_exp }
end

end hF

section nums

lemma coe_659 : ((659 : fin 660) : ℕ) = 659 :=
begin
rw [fin.coe_bit1, fin.coe_bit1, fin.coe_bit0, fin.coe_bit0, fin.coe_bit1,
fin.coe_bit0, fin.coe_bit0, fin.coe_bit1, fin.coe_bit0],
simp only [fin.coe_one],
all_goals { dec_trivial }
end

lemma pos_660 : (0 : ℕ) < 660 := dec_trivial

lemma posQ_660 : (0 : ℚ) < 660 := nat.cast_lt.mpr pos_660

lemma expand (d : fin 660) : hF 660 d + hF 660 (659 - d) = 1979 / ((660 + d) * (1319 - d)) :=
begin
obtain ⟨d, dlim⟩ := d,
simp only [hF, one_div],
simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk, fin.coe_sub, coe_659,
nat.cast_sub (nat.le_of_succ_le_succ dlim), coe_coe],
refine congr_arg2 has_div.div _ _,
norm_num },
norm_num },
{ simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
{ simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
end

lemma sub_659 : fin.last 659 = (659 : fin 660) - (0 : fin 660) := rfl

end nums

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x : fin 1320, h x
→ 1979 ∣ p :=
begin
intro F,
rw (show 1320 = 660 * 2, by norm_num) at F,
rw h_to_hF at F,
rw fin.sum_univ_cast_succ at F,
rw fin.sum_univ_succ at F,
rw add_comm (∑ _, _) at F,
rw sub_659 at F,
rw fin.cast_succ_zero at F,
rw expand 0 at F,
sorry,
end


#### Miroslav Olšák (Sep 27 2020 at 09:48):

As we were discussing that it could be just easily canlculated, how could one prove that?:

example : (∑ n in finset.range 1320, ((-1)^(n + 1) / n : ℚ))
=
(9712435370176457211789032112275705035436058023056668172162691122769643536134963388887418503518212227707181887399284421324209991580261372180881066042267340013822543021630993790301871917306672479003742347731906894502206611684973377349822140727866748793472314555146081954133359219693224842345716201562838113110488664229990443258508595332395129617286143580898566908128232436187466371871641095608257859832669859587159077972843255741143946005144546720084104126426401254209483858435525146637078869452056788708944608960016712180409515668301909686056363654039823351264466923197720153813
/
14004426370194880461934343682044774391282833031127910746297786781959105584828861694180270900155320736866485178357969757814225700469374818454186270560156419686116542029027696742870488277713573014598870206397512488706141517193426122086231634178080237723065448682598131182597623527313179068878231298472650458406330723014358986732179004322578669107971003162372262774921109835980551500767898797452304799628071849186633284721093163439037683000781898695594646092124867941059532453140720984993275703737648888419223774236963722967299484493466538792766661068428697404447683623975519360000 : ℚ)
:=


#### Kenny Lau (Sep 27 2020 at 09:58):

does by norm_num work?

I'm guessing no

#### Kevin Buzzard (Sep 27 2020 at 10:14):

But pari does it in a split second

#### Rob Lewis (Sep 27 2020 at 10:20):

In principle this works -- it reduces things to the scope of norm_num. But norm_num uses too much memory for VSCode. Maybe if you run it with a higher memory limit, or do something clever to simplify intermediate steps, you could make it work. (Not in a split second.)

import algebra.big_operators.finsupp data.rat

open_locale big_operators

example : (∑ n in finset.range 1320, ((-1)^(n + 1) / n : ℚ))
=
(9712435370176457211789032112275705035436058023056668172162691122769643536134963388887418503518212227707181887399284421324209991580261372180881066042267340013822543021630993790301871917306672479003742347731906894502206611684973377349822140727866748793472314555146081954133359219693224842345716201562838113110488664229990443258508595332395129617286143580898566908128232436187466371871641095608257859832669859587159077972843255741143946005144546720084104126426401254209483858435525146637078869452056788708944608960016712180409515668301909686056363654039823351264466923197720153813
/
14004426370194880461934343682044774391282833031127910746297786781959105584828861694180270900155320736866485178357969757814225700469374818454186270560156419686116542029027696742870488277713573014598870206397512488706141517193426122086231634178080237723065448682598131182597623527313179068878231298472650458406330723014358986732179004322578669107971003162372262774921109835980551500767898797452304799628071849186633284721093163439037683000781898695594646092124867941059532453140720984993275703737648888419223774236963722967299484493466538792766661068428697404447683623975519360000 : ℚ)
:=
begin
iterate 1320
{ transitivity,
apply finset.sum_range_succ,
rw finset.sum_range_zero,
simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_add, nat.cast_zero, nat.cast_one],
-- norm_num1,
end


#### Miroslav Olšák (Sep 27 2020 at 13:09):

Would it be possible to tell lean to just call #eval to the first expression?

#### Scott Morrison (Sep 27 2020 at 13:17):

Sure. But #eval is just a calculator; no proofs attached.

#### Yakov Pechersky (Sep 27 2020 at 15:27):

All that's left to do is change the divisibility goal to be on Q instead of N:

import tactic.ring_exp
import data.matrix.notation
import data.rat.cast

open_locale big_operators

def h {n : ℕ} : fin n → ℚ := λ k, (-1)^((k : ℕ)+ 1)/k

instance foo : fact (nat.prime 1979) := by norm_num

@[simp] lemma fin.coe_sub {n : ℕ} (x y : fin n) : (((x - y) : fin n) : ℕ) = (x : ℕ) - y :=
by { cases x, cases y, refl }

lemma fin.coe_bit0 {n : ℕ} {x : fin n} (h : (bit0 x : ℕ) < n) : ((bit0 x : fin n) : ℕ) = bit0 x :=
by { cases x, exact nat.mod_eq_of_lt h }

lemma fin.coe_bit1 {n : ℕ} {x : fin (n + 2)} (h : (bit1 x : ℕ) < n + 2) :
((bit1 x : fin (n + 2)) : ℕ) = bit1 x :=
begin
rw bit1 at h,
fin.coe_bit0 (lt_of_le_of_lt (nat.le_add_right _ _) h)] using nat.mod_eq_of_lt h,
end

lemma nat.le_add (n m : ℕ) : n ≤ n + m :=
nat.le.intro rfl

section hF

variables {n : ℕ} (N : ℕ) (x : fin n)

def hF : ℚ := 1 / ((N + (x : ℕ)) : ℚ)

lemma shift : hF N.succ x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma shift' : hF (N + 1) x.cast_succ = hF N x.succ :=
by { simp [hF], ring_exp }

lemma reduce : @hF n.succ N x.cast_succ = @hF n N x :=
by simp [hF]

lemma hreduce : h x.cast_succ.cast_succ = h x :=
by simp [h]

lemma h_to_hF : (∑ x : fin (N * 2), h x) = ∑ x : fin N, hF N x :=
begin
induction N with N hN,
{ refl },
symmetry,
rw fin.sum_univ_cast_succ,
simp_rw shift N,
simp_rw reduce,
symmetry,
rw [nat.succ_mul, fin.sum_univ_cast_succ, fin.sum_univ_cast_succ],
simp_rw hreduce,
congr' 1,
congr,
{ have nh : (-1 : ℚ) ^ (N * 2 + 1) = -1,
{ rw [mul_comm],
have : (N : ℚ)⁻¹ = 2 / (N * 2),
{ norm_num [←one_div, mul_comm, div_mul_eq_div_mul_one_div] },
norm_num [h, hF, nh, this],
ring_exp },
{ have nh : (-1 : ℚ) ^ (N * 2 + 1 + 1) = 1,
{ rw [mul_comm],
norm_num [h, hF, nh],
ring_exp }
end

end hF

section nums

lemma coe_659 : ((659 : fin 660) : ℕ) = 659 :=
begin
rw [fin.coe_bit1, fin.coe_bit1, fin.coe_bit0, fin.coe_bit0, fin.coe_bit1,
fin.coe_bit0, fin.coe_bit0, fin.coe_bit1, fin.coe_bit0],
simp only [fin.coe_one],
all_goals { dec_trivial }
end

lemma pos_660 : (0 : ℕ) < 660 := dec_trivial

lemma posQ_660 : (0 : ℚ) < 660 := nat.cast_lt.mpr pos_660

lemma expand (d : fin 660) : hF 660 d + hF 660 (659 - d) = 1979 / ((660 + d) * (1319 - d)) :=
begin
obtain ⟨d, dlim⟩ := d,
simp only [hF, one_div],
simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk, fin.coe_sub, coe_659,
nat.cast_sub (nat.le_of_succ_le_succ dlim), coe_coe],
refine congr_arg2 has_div.div _ _,
norm_num },
norm_num },
{ simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
norm_cast,
exact ne_of_gt (lt_of_lt_of_le pos_660 (nat.le_add 660 d)) },
{ simp only [nat.cast_bit0, nat.cast_bit1, nat.cast_one, fin.coe_mk],
refine ne_of_gt (lt_of_lt_of_le posQ_660 _),
end

lemma expand' (d : ℕ) (h : d < 331) :
(∑ x : fin (d * 2), hF (990 - d) x) = ∑ x : fin d, ((1979 : ℚ) / ((990 + (x : ℕ)) * (989 - (x : ℕ)))) :=
begin
induction d with d hd,
{ rw zero_mul,
simp only [fin.sum_univ_zero] },
{ have h' := nat.lt_of_succ_lt h,
have h'' := nat.mul_lt_mul h' (le_refl 2) (by dec_trivial),
have h''' := nat.mul_lt_mul h (le_refl 2) (by dec_trivial),
rw nat.succ_mul at h''',
rw nat.succ_mul,
rw fin.sum_univ_succ,
rw fin.sum_univ_cast_succ,
simp_rw ←shift',
simp_rw reduce,
have : 990 - d.succ + 1 = 990 - d,
{ rw ←nat.sub_sub_assoc,
refl,
refine le_of_lt (lt_trans h _),
norm_num,
exact nat.succ_pos' },
rw this,
clear this,
rw hd h',
rw fin.sum_univ_cast_succ,
congr' 1,
simp only [hF, one_div, add_zero, fin.coe_zero, nat.succ_sub_succ_eq_sub, fin.coe_last, nat.cast_bit0, nat.cast_zero,
nat.cast_one, nat.cast_mul],
rw mul_two,
norm_cast,
have le990 : d ≤ 990,
{ refine le_of_lt (lt_trans h' _),
norm_num },
have le989 : d ≤ 989,
{ refine le_of_lt (lt_trans h' _),
norm_num },
refine congr_arg2 has_div.div _ _,
{ norm_cast,
norm_num },
{ norm_cast },
{ rw nat.cast_ne_zero,
refine ne_of_gt (lt_of_lt_of_le _ (nat.le_add 990 d)),
norm_num },
{ rw nat.cast_ne_zero,
refine ne_of_gt _,
refine nat.sub_pos_of_lt _,
refine lt_trans h' _,
norm_num } }
end

lemma sub_659 : fin.last 659 = (659 : fin 660) - (0 : fin 660) := rfl

end nums

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ x : fin 1320, h x
→ 1979 ∣ p :=
begin
intro F,
rw (show 1320 = 660 * 2, by norm_num) at F,
rw h_to_hF at F,
rw (show 660 = 330 * 2, by norm_num) at F,
have : ∀ x : fin (330 * 2), hF (330 * 2) x = hF (990 - 330) x,
{ intro x,
simp_rw (show 330 * 2 = 990 - 330, by norm_num) },
simp_rw this at F,
rw expand' 330 (by norm_num) at F,
simp_rw division_def at F,
rw ←finset.mul_sum at F,
set S := (∑ (x : fin 330), (((990 : ℚ) + x) * (989 - x))⁻¹) with hS,
simp_rw [coe_coe] at hS,
rw ←hS at F,
sorry
/-
p q : ℕ,
this : ∀ (x : fin (330 * 2)), hF (330 * 2) x = hF (990 - 330) x,
S : ℚ := ∑ (x : fin 330), ((990 + ↑x) * (989 - ↑x))⁻¹,
hS : S = ∑ (x : fin 330), ((990 + ↑↑x) * (989 - ↑↑x))⁻¹,
F : ↑p * (↑q)⁻¹ = 1979 * S
⊢ 1979 ∣ p
-/

end


#### Yakov Pechersky (Sep 27 2020 at 15:27):

Can definitely be cleaned up.

#### Kevin Buzzard (Sep 27 2020 at 15:44):

I tried with the finset approach (no fin) and it ended up looking like this:

import tactic
import algebra.big_operators.ring
import data.nat.parity
import data.finset.intervals

open_locale big_operators

open finset

open nat

instance foo : fact (nat.prime 1979) := by norm_num

open finset

--example (k : Type) [comm_ring k] (a b : k) : k := a - b

namespace imo1979q1

-- some constants
@[reducible] def a : ℚ := ∑ n in range 1320, (-1)^(n + 1) / n
@[reducible] def b : ℚ := ∑ n in range 1320, 1 / n
@[reducible] def c : ℚ := ∑ n in range 660, 1 / n
@[reducible] def d : ℚ := ∑ n in Ico 660 1320, 1 / n
@[reducible] def e : ℚ := ∑ n in range 330, 1 / (n + 660)
@[reducible] def f : ℚ := ∑ n in range 330, 1 / (1319 - n)

/-

Lemma 1 : b - a = c
Lemma 2 : c + d = b (and hence a = d)
Lemma 3 : d = e + f

Then we prove the theorem, by showing the 1979-adic
valuation of e + f is positive.
-/

@[reducible] def double : ℕ ↪ ℕ := ⟨λ n, 2 * n, λ a b, mul_left_cancel' (by norm_num)⟩
--@[reducible] def
lemma lemma1 : b - a = c :=
calc b - a = ∑ n in range 1320, (1/n - (-1)^(n+1)/n) : by rw sum_sub_distrib
... = ∑ n in range 1320, ite (even n) (2/n) 0 : by {
apply sum_congr rfl,
rintros x hx,
split_ifs,
{ rcases h with ⟨n, rfl⟩,
rw [pow_mul, pow_two],
simp, norm_num },
{ rw not_even_iff at h,
have h8 := nat.mod_add_div x 2,
rw h at h8,
suffices : (1 : ℚ) + (-1)^x = 0,
rw this, simp,
rw ← h8,
}
}
... = ∑ (x : ℕ) in filter even (range 1320), 2 / x : by rw sum_filter
... = ∑ (x : ℕ) in map double (range 660), (2 : ℚ) / x : by {
-- extract_goal, -- problem not observed
apply sum_congr, swap, simp,
apply finset.subset.antisymm,
{ --extract_goal, -- problem not observed
intros x hx,
rw mem_filter at hx,
rcases hx with ⟨hx1, m, rfl⟩,
rw mem_map,
--extract_goal, -- problem not observed
-- uncommenting this times out
-- use m,                          -- << timeout
existsi m, -- works fine
existsi _, refl,
rw mem_range at hx1 ⊢,
linarith },
{ intros x hx,
rw mem_filter,
rw mem_map at hx,
rcases hx with ⟨a, ha, rfl⟩,
split,
{ rw mem_range at ha ⊢,
change 2 * a < 1320,
linarith },
{ existsi a,
refl
}
}
}
... = c : by {
rw sum_map (range 660) double (λ n, (2 : ℚ) / n),
apply sum_congr, refl, -- is there a better way?
intros x hx,
show (2 : ℚ) / (2 * x : ℕ) = _,
push_cast,
change (2 : ℚ) / (2 * x) = 1 / x,
generalize h : (x : ℚ) = q,
by_cases hq : q = 0,
rw hq, ring,
field_simp [hq] }

lemma lemma2 : c + d = b :=
begin
unfold c d b,
simp only [← Ico.zero_bot],
rw ← sum_union,
{ apply sum_congr,
{ ext x,
suffices : x < 660 ∨ 660 ≤ x ∧ x < 1320 ↔ x < 1320,
simpa,
split,
{ rintro (a | ⟨b, c⟩); linarith },
{ intro hx,
cases lt_or_le x 660,
{ left, assumption },
{ right, cc } } },
{ intros, refl } },
apply Ico.disjoint_consecutive
end

lemma corollary3 : a = d :=
begin
rw lemma2,
rw ← lemma1,
end

lemma lemma4 : e + f = d :=
begin
unfold d e f,
rw (Ico.zero_bot 330).symm,
have h : ∑ (n : ℕ) in Ico 0 330, (1 : ℚ) / (n + 660) =
∑ (m : ℕ) in Ico 660 990, (1 : ℚ) / m,
{
rw sum_image,
{ apply sum_congr, refl,
{ intros x hx y hy,
},
rw h, clear h,
have h : ∑ (n : ℕ) in Ico 0 330, (1 : ℚ) / (1319 - n) =
∑ (m : ℕ) in Ico 990 1320, (1 : ℚ) / m,
{ have h2 : image (λ (j : ℕ), 1319 - j) (Ico 0 330) =
Ico (990) (1320),
{ rw Ico.image_const_sub, refl, linarith },
rw ← h2,
rw sum_image,
{ apply sum_congr, refl,
intros,
apply congr_arg,
rw nat.cast_sub, norm_cast,
rw Ico.mem at H,
cases H, linarith },
{ intros x hx y hy,
intro h,
rw [Ico.zero_bot, mem_range] at hx hy,
rw nat.sub_eq_iff_eq_add (show x ≤ 1319, by linarith) at h,
symmetry' at h,
rw nat.sub_eq_iff_eq_add at h, swap, linarith,
},
rw h, clear h,
rw ←sum_union,
{ apply sum_congr,
{ apply Ico.union_consecutive; linarith },
{ intros, refl } },
{ apply Ico.disjoint_consecutive }
end

lemma lemma5 : ∀ n ∈ range 330, ∥ (((1 / (n + 660) + 1 / (1319 - n)) : ℚ) : ℚ_[1979]) ∥ < 1 :=
begin
intros n hn,
rw mem_range at hn,
have h1 : (n : ℚ) + 660 ≠ 0,
apply ne_of_gt,
norm_cast, simp,
have h2 : (1319 : ℚ) - n ≠ 0,
have h3 : (n : ℚ) < 330, norm_cast, exact hn,
linarith,
let p : ℕ := 1979,
have h3 : (1 : ℚ) / (n + 660) + 1 / (1319 - n) = 1979 / ((n + 660) * (1319 - n)),
field_simp [h1, h2],
generalize : (n : ℚ) = q,
ring,
rw h3, clear h3,
push_cast,
rw normed_field.norm_div,
rw normed_field.norm_mul,
rw div_lt_one,
sorry,
sorry,
end

theorem imo (p q : ℕ) : (p : ℚ) / q =
-- 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319),
∑ n in finset.range 1320, (-1)^(n + 1) / n
→ 1979 ∣ p :=
begin
change _ = a → _,
rw corollary3,
rw ← lemma4,
intro h,
unfold e f at h,

sorry
end

end imo1979q1


I'm not finished either -- I'm at the same place as you in fact.

#### Kevin Buzzard (Sep 27 2020 at 15:44):

I just decided it was time I learnt about how sums work in Lean nowadays :-)

#### Yakov Pechersky (Sep 27 2020 at 15:50):

I think the solution for my approach is to somehow identify q with the product of 660 to 1320. And then push the casts to remove the casts to Q and make everything statements about N.

#### Kevin Buzzard (Sep 27 2020 at 15:51):

My gut feeling is that using p-adic norm should make life easier; you don't have to deal with the denominator that way.

Last updated: May 10 2021 at 08:14 UTC