Zulip Chat Archive

Stream: maths

Topic: IMO2019


view this post on Zulip Kevin Buzzard (Aug 01 2019 at 19:42):

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?

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 19:42):

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

view this post on Zulip Johan Commelin (Aug 01 2019 at 19:43):

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

view this post on Zulip Floris van Doorn (Aug 01 2019 at 19:44):

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

view this post on Zulip Johan Commelin (Aug 01 2019 at 19:45):

Aah, right. So nr2 and nr6 are also dec_trivial

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 19:55):

Great, so only two problems left!

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 19:56):

And Reid has nearly done one of them

view this post on Zulip Patrick Massot (Aug 01 2019 at 21:15):

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?

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 21:45):

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.

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 21:45):

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 :-)

view this post on Zulip Patrick Massot (Aug 01 2019 at 21:46):

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

view this post on Zulip Patrick Massot (Aug 01 2019 at 21:47):

random hit from google "formalization area method"

view this post on Zulip Kevin Buzzard (Aug 01 2019 at 22:19):

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

view this post on Zulip Scott Morrison (Aug 01 2019 at 22:45):

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?

view this post on Zulip Reid Barton (Aug 01 2019 at 23:50):

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

view this post on Zulip Reid Barton (Aug 01 2019 at 23:51):

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

view this post on Zulip Reid Barton (Aug 01 2019 at 23:52):

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

view this post on Zulip Floris van Doorn (Aug 02 2019 at 00:33):

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!.

view this post on Zulip Reid Barton (Aug 02 2019 at 00:58):

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

view this post on Zulip Reid Barton (Aug 02 2019 at 01:04):

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

view this post on Zulip Reid Barton (Aug 02 2019 at 01:04):

Though I don't think anyone proved it

view this post on Zulip Johan Commelin (Aug 02 2019 at 05:44):

padic_val is defined in terms of multiplicity.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 10:05):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:01):

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...

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:07):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:07):

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?

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:08):

the get is roption.get

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:09):

hmm, h1 might be a coe from nat to int

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:23):

rw coe_lt_coe at h1?

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:24):

Where is the proof that goes into the get _?

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:24):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:24):

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

view this post on Zulip Chris Hughes (Aug 02 2019 at 11:24):

convert h1; exact option.some_get _?

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:24):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:25):

convert h1 fails horribly with goals like int = enat

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:25):

I'm making progress though.

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:25):

Ah, there is also multiplicity.nat_eq_int or whatever.

view this post on Zulip Chris Hughes (Aug 02 2019 at 11:25):

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

view this post on Zulip Chris Hughes (Aug 02 2019 at 11:26):

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

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:26):

int.coe_nat_multiplicity

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:42):

I've got it down to

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:46):

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)

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:49):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:50):

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

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:51):

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

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:52):

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

@Kevin Buzzard does this help :up:

view this post on Zulip Johan Commelin (Aug 02 2019 at 11:53):

Ooh, wait. You already found a proof.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:53):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:53):

Yes, there are no sorries in the gist.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:54):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:55):

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

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:57):

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.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:58):

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.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 12:00):

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?

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 12:01):

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.

view this post on Zulip Reid Barton (Aug 02 2019 at 12:42):

Looks like a good start though. There was some discussion earlier about the best way to even write down the answer j1n/pj\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 pp) and sometimes it might be the most convenient form to use as well.

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 12:45):

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.

view this post on Zulip Reid Barton (Aug 02 2019 at 13:09):

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

view this post on Zulip Floris van Doorn (Aug 02 2019 at 14:57):

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

view this post on Zulip Floris van Doorn (Aug 02 2019 at 20:28):

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.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 20:29):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 02 2019 at 20:29):

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

view this post on Zulip Floris van Doorn (Aug 02 2019 at 23:07):

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.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:32):

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

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:32):

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

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:33):

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

view this post on Zulip Patrick Massot (Aug 06 2019 at 18:24):

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

view this post on Zulip Patrick Massot (Aug 06 2019 at 18:25):

For the record, Kevin:

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

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 19:32):

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?


Last updated: May 18 2021 at 06:15 UTC