IMO2019

Stream: maths

[Kevin Buzzard]

It's silly talking about IMO2019 in three different threads none of which are in #maths . When I was a kid I always used to feel that "every geometry problem can be solved using coordinates". Is that true? I would imagine this sort of thing is well-understood nowadays. My feeling was that you just bash everything out and you end up having to prove something of the form X=X. What is actually going on? In particular, is the analytic approach to Q2 and Q6 "doomed to succeed" in some sense?

[Kevin Buzzard]

https://www.imo-official.org/year_info.aspx?year=2019

[Johan Commelin]

Didn't Tarski prove that Euclidean geometry is decidable? That's what you were alluding to with the dec_trivial, right?

[Floris van Doorn]

The dec_trivial was about the graph theory problem, which is indeed a finite search problem...

[Johan Commelin]

Aah, right. So nr2 and nr6 are also dec_trivial

[Kevin Buzzard]

Great, so only two problems left!

[Kevin Buzzard]

And Reid has nearly done one of them

[Patrick Massot]

I don't know anything about IMO, but I guess proofs by dec_trivial do not qualify. Would you get points for transcribing an exhaustive search or something like that? Or is it a virtual question because this would take way too much time in practice?

[Kevin Buzzard]

Yes exactly, it will probably take longer than the lifespan of the earth to do it by dec_trivial. But of course this is just a tedious implementation issue.

[Kevin Buzzard]

Actually maybe the geometry ones could really be done by just bashing out the algebra. I've done olympiad problems in the past that way. It was the only technique I knew :-)

[Patrick Massot]

See also https://dpt-info.u-strasbg.fr/~narboux/area_method.html

[Patrick Massot]

random hit from google "formalization area method"

[Kevin Buzzard]

Manual Eberl's Isabelle effort for Q1 -- much shorter. http://downthetypehole.de/paste/4YbGgqb4

[Scott Morrison]

I see some auto and some blast in there; can Kevin or Reid tell us "which parts" of their proofs are being handled by these?

[Reid Barton]

The auto on line 24 corresponds to the stuff I do starting have hf₀ := hf 0 0, in order to solve the equations $c^2 = 2c$ and $2d=cd$

[Reid Barton]

I don't see how the blast on line 34 does anything interesting at all, it looks like we did all the work earlier

[Reid Barton]

Some of the other auto/simp handles some linear combinations of equations and algebraic simplification which I wasn't too happy about in my version

[Floris van Doorn]

Making good progress on IMO 2019-4: https://gist.github.com/fpvandoorn/e0bd9d116a59a5f01d1d661f3677b72f

The main argument is there. The main missing ingredient is that multiplicity 2 n.fact < n, i.e. there are less than n factors of 2 in n!.

[Reid Barton]

I think your sorried lemmas about multiplicity already exist for padic_val, is that known to be the same as multiplicity?

[Reid Barton]

The theorem about the multiplicity of primes in factorials was discussed here around the end of May I think

[Reid Barton]

Though I don't think anyone proved it

[Johan Commelin]

padic_val is defined in terms of multiplicity.

[Kevin Buzzard]

The main argument is there. The main missing ingredient is that multiplicity 2 n.fact < n, i.e. there are less than n factors of 2 in n!.

I'm having a go at this, but note that the actual sorried lemma in the gist is false for n=0

[Kevin Buzzard]

import data.padics imo2019_4

instance two_prime : nat.prime 2 := by norm_num

lemma aux1 (n : ℕ) : padic_val_rat 2 (n + 1).fact = padic_val_rat 2 (n + 1) + padic_val_rat 2 n.fact :=
begin
  rw (show (n + 1).fact = (n + 1) * n.fact, from rfl),
  rw nat.cast_mul,
  rw padic_val_rat.mul 2,
  refl,
  -- side conditions
  norm_cast, exact dec_trivial,
  norm_cast, have := nat.fact_pos n, linarith, -- I have no shame
end

lemma aux2 (d : ℕ) : padic_val_rat 2 (2 * d + 1 : ℕ) = 0 :=
begin
show padic_val_rat 2 ((2 * d + 1) : ℤ) = 0,
  rw padic_val_rat.padic_val_rat_of_int,
  norm_cast,
  convert enat.get_zero _,
  apply multiplicity.multiplicity_eq_zero_of_not_dvd,
  rintro ⟨c, hc⟩,
  apply @zero_ne_one ℕ,
  calc 0 = (2 * c) % 2 : (nat.mul_mod_right _ _).symm
  ...    = (2 * d + 1) % 2 : by rw hc
  ...    = _ : nat.mod_two_of_bodd (2 * d + 1)
  ...    = 1 : by simp,
  -- now pick up the pieces
  all_goals {exact dec_trivial},
end

lemma two_adic_val_fact_even (n : ℕ) : padic_val_rat 2 ((2 * n).fact) = n + padic_val_rat 2 n.fact :=
begin
  induction n with d hd,
    show padic_val_rat 2 1 = 0 + padic_val_rat 2 1,
    rw zero_add,
  rw (show 2 * nat.succ d = 2 * d + 1 + 1, by ring),
  rw [aux1, aux1, hd],
  norm_cast,
  rw (show 2 * d + 1 + 1 = 2 * (d + 1), by ring),
  rw nat.cast_mul,
  rw padic_val_rat.mul 2,
  rw padic_val_rat.padic_val_rat_self,
  rw (show nat.succ d = d + 1, from rfl),
  rw aux1,
  rw aux2,
  simp,
  all_goals {try {norm_cast}, exact dec_trivial},
end

lemma two_adic_val_fact_odd (n : ℕ) : padic_val_rat 2 ((2 * n + 1).fact) = n + padic_val_rat 2 n.fact :=
begin
  rw aux1,
  convert two_adic_val_fact_even n,
  convert zero_add _,
  convert aux2 n,
end

lemma even_or_odd (n : ℕ) : ∃ c, n = 2 * c ∨ n = 2 * c + 1 :=
begin
  induction n with d hd,
    use 0, left, refl,
  cases hd with e he,
  cases he,
    use e, right, rw he,
  use (e + 1), left, rw he, ring,
end

lemma two_adic_val_fact (d : ℕ) : padic_val_rat 2 d.fact = d / 2 + padic_val_rat 2 (d / 2).fact :=
begin
  cases (even_or_odd d) with n hn,
  cases hn,
  { rw hn,
    convert two_adic_val_fact_even n,
      norm_cast,
    all_goals {rw [mul_comm, nat.mul_div_cancel], exact dec_trivial},
  },
  { rw hn,
    convert two_adic_val_fact_odd n,
      norm_cast,
    all_goals {rw [add_comm, nat.add_mul_div_left], convert zero_add _, exact dec_trivial},
  }
end

lemma easy (n : ℕ) : n / 2 + n / 2 ≤ n :=
begin
  cases even_or_odd n,
  cases h,
    rw [h, nat.mul_div_right], linarith, exact dec_trivial,
  rw add_comm at h,
  rw h,
  rw nat.add_mul_div_left,
  rw (show 1 / 2 = 0, from dec_trivial),
  linarith, -- finally!
  exact dec_trivial,
end

lemma two_adic_val_fact_lt (n : ℕ) (h : n ≠ 0) :
  padic_val_rat 2 n.fact < n :=
begin
  revert h,
  apply nat.strong_induction_on n, clear n,
  intros m hm,
  by_cases h1 : m = 1,
    intro h0, rw h1,
    show padic_val_rat 2 1 < 1,
    rw padic_val_rat.one, exact dec_trivial,
  intro h,
  rw two_adic_val_fact m,
  have := hm (m / 2) _ _,
  refine lt_of_lt_of_le (add_lt_add_left this _) _,
  norm_cast,
  exact easy m,
  rw nat.div_lt_iff_lt_mul',
  rw mul_two,
  apply nat.lt_add_of_zero_lt_left,
  exact nat.pos_of_ne_zero h,
  -- now pick up the pieces
    exact dec_trivial,
  intro h2,
  rw nat.div_eq_zero_iff at h2,
  cases h2 with c hc, apply h1, refl,
  cases hc with d hd, apply h, refl,
  cases hd,
  exact dec_trivial,
end

There's the proof for p=2 but using padic_val_rat. It's dirty but it works. Now I need to convince Lean that multiplicity (taking values in enat) and padic_val_rat (taking values in int) are the same...

[Johan Commelin]

Isn't padic_val defined in terms of multiplicity? So I would hope that after unfolding some definitions norm_cast can do this.

[Kevin Buzzard]

h1 : ↑((multiplicity ↑2 ↑(nat.fact n)).get _) < ↑n
⊢ multiplicity 2 (nat.fact n) < ↑n

h1 is about int, and the goal is about enat. What do you think?

[Kevin Buzzard]

the get is roption.get

[Kevin Buzzard]

hmm, h1 might be a coe from nat to int

[Johan Commelin]

rw coe_lt_coe at h1?

[Johan Commelin]

Where is the proof that goes into the get _?

[Kevin Buzzard]

The problem is the _. I've made progress.

[Kevin Buzzard]

Yes exactly, one has to supply that proof explicitly it seems.

[Chris Hughes]

convert h1; exact option.some_get _?

[Johan Commelin]

Because rw [← enat.coe_get ThatProof, enat.coe_lt_coe] will also help.

[Kevin Buzzard]

convert h1 fails horribly with goals like int = enat

[Kevin Buzzard]

I'm making progress though.

[Johan Commelin]

Ah, there is also multiplicity.nat_eq_int or whatever.

[Chris Hughes]

There's some int coercions i didn't see.

[Chris Hughes]

So there's a lemma to prove about multiplicity being preseved along injective monoid homs I guess.

[Johan Commelin]

int.coe_nat_multiplicity

[Kevin Buzzard]

I've got it down to

⊢ ∀ (m : enat) (n : ℕ) (h : m.dom), m.get h < n → m < ↑n

[Kevin Buzzard]

I'm hoping this is true, because modulo this I have

lemma multiplicity_two_fact_lt (n : ℕ) (h : n ≠ 0) :
  multiplicity 2 n.fact < n

which is hopefully enough for @Floris van Doorn (note h)

[Kevin Buzzard]

lemma aux_53 : ∀ (m : enat) (n : ℕ) (h : m.dom), m.get h < n → m < (n : enat) :=
begin
  intros,
  rw (show m = m.get h, by simp),
  norm_cast, assumption,
end

[Kevin Buzzard]

https://gist.github.com/kbuzzard/4ca88f429bda4744fd038f7471ebfb67

@Floris van Doorn @Reid Barton -- it's a mess, but hopefully it helps.

[Kevin Buzzard]

@Paul-Nicolas Madelaine I used norm_cast 11 times! Thank you so much!

[Johan Commelin]

Because rw [← enat.coe_get ThatProof, enat.coe_lt_coe] will also help.

@Kevin Buzzard does this help :up:

[Johan Commelin]

Ooh, wait. You already found a proof.

[Kevin Buzzard]

Yes, what you and Chris said helped a great deal.

[Kevin Buzzard]

Yes, there are no sorries in the gist.

[Kevin Buzzard]

It feels a bit dirty not doing something for general p (I guess $n >0 \implies v_p(n!)<n/(p-1)$) but we only need it for p=2 for the IMO problem.

[Kevin Buzzard]

p=2 makes life much easier because one doesn't have to venture into rat.

[Kevin Buzzard]

and one can just use the dirty fact that every integer is either even or odd, and the 2-adic valuation of an odd integer is 0. The general proof will be more painful for both of these reasons.

[Kevin Buzzard]

I'm going to leave this now because unfortunately I have literally hundreds of unread emails which need dealing with, but this experience showed me that we seem to be missing a bunch of lemmas all over the place.

[Kevin Buzzard]

I used padic_val_rat because results like padic_val_rat.mul were proved (which are not true for general n-adic valuations if n isn't irreducible). Is there an analogous result for multiplicity in e.g. a UFD?

[Kevin Buzzard]

If there is then I suspect that one could have used multiplicity all the way through, but I suspect it would have been no easier or harder. The proof needs a huge tidy.

[Reid Barton]

Looks like a good start though. There was some discussion earlier about the best way to even write down the answer $\sum_{j \ge 1} \lfloor n/p^j \rfloor$.
Your two_adic_val_fact (d : ℕ) : padic_val_rat 2 d.fact = d / 2 + padic_val_rat 2 (d / 2).fact is a nice intermediate statement to aim for (for general $p$) and sometimes it might be the most convenient form to use as well.

[Kevin Buzzard]

That was the reason I put the time in. I was initially thinking "eew, you can't prove this by induction, it's kind of nasty" but then when I realised that the intermediate statement was provable by the case split into even and odd and then induction, and the result we needed followed from that and strong induction, I thought I'd go for it. Probably I should have done everything using multiplicity.

[Reid Barton]

Right, I see in a couple places you did 2 things where in general you would have to do $p$ things. But it's probably not that hard to do little inductions from $p*n$ up to $p*n + r$ for $0 \le r < p$

[Floris van Doorn]

Very nice, @Kevin Buzzard. Thanks! I indeed have the assumption that n > 0, so adding that assumption (that I missed) is indeed no problem.

[Floris van Doorn]

I finished the proof of IMO 2019-4! :tada: https://gist.github.com/fpvandoorn/e0bd9d116a59a5f01d1d661f3677b72f

Not all lemmas I prove in that file are used. Once I started proving lemma's about multiplicity/enat/roption, I decided to also prove all similar missing lemmas. I'll PR them to mathlib at some point.

[Floris van Doorn]

I'm importing Kevin's file in that Gist.

[Bryan Gin-ge Chen]

Should we have a leanprover-community/lean-imo repository?

[Floris van Doorn]

That's one possibility.
I will make a PR to mathlib soon adding a new top-level folder where we can put one-off projects like this. I think when we talked about this earlier the consensus was to have projects like these in mathlib, but not in the src/ folder, so that we can make sure that files like this keep compiling.

[Mario Carneiro]

IMO2019-4 just appeared in the AFP along with 1 and 5. I guess it's the year of the contest problem...

[Kevin Buzzard]

Yeah, Manuel Eberl saw me going on about Q1 on Twitter.

[Kevin Buzzard]

https://mathoverflow.net/questions/337558/automatically-solving-olympiad-geometry-problems?noredirect=1#comment844402_337558 That was me trying to work out how to do Q2 and Q6

[Patrick Massot]

Manuel was even seen here at the time we were discussing IMO

[Patrick Massot]

For the record, Kevin:

See also https://dpt-info.u-strasbg.fr/~narboux/area_method.html

[Kevin Buzzard]

Aah, that link makes a lot more sense now I know what the area method is! Thanks Patrick. Sorry I missed it the first time around. So maybe the Coq people can do Q2?