# Zulip Chat Archive

## Stream: maths

### Topic: IMO2019

#### 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?

#### Kevin Buzzard (Aug 01 2019 at 19:42):

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

#### 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?

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

#### Johan Commelin (Aug 01 2019 at 19:45):

Aah, right. So nr2 and nr6 are also `dec_trivial`

#### Kevin Buzzard (Aug 01 2019 at 19:55):

Great, so only two problems left!

#### Kevin Buzzard (Aug 01 2019 at 19:56):

And Reid has nearly done one of them

#### 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?

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

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

#### Patrick Massot (Aug 01 2019 at 21:46):

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

#### Patrick Massot (Aug 01 2019 at 21:47):

random hit from google "formalization area method"

#### Kevin Buzzard (Aug 01 2019 at 22:19):

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

#### 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?

#### 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 $c^2 = 2c$ and $2d=cd$

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

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

#### 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!`

.

#### 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`

?

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

#### Reid Barton (Aug 02 2019 at 01:04):

Though I don't think anyone proved it

#### Johan Commelin (Aug 02 2019 at 05:44):

`padic_val`

is defined in terms of `multiplicity`

.

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

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

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

#### 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?

#### Kevin Buzzard (Aug 02 2019 at 11:08):

the `get`

is `roption.get`

#### Kevin Buzzard (Aug 02 2019 at 11:09):

hmm, `h1`

might be a coe from nat to int

#### Johan Commelin (Aug 02 2019 at 11:23):

`rw coe_lt_coe at h1`

?

#### Johan Commelin (Aug 02 2019 at 11:24):

Where is the proof that goes into the `get _`

?

#### Kevin Buzzard (Aug 02 2019 at 11:24):

The problem is the `_`

. I've made progress.

#### Kevin Buzzard (Aug 02 2019 at 11:24):

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

#### Chris Hughes (Aug 02 2019 at 11:24):

`convert h1; exact option.some_get _`

?

#### Johan Commelin (Aug 02 2019 at 11:24):

Because `rw [← enat.coe_get ThatProof, enat.coe_lt_coe]`

will also help.

#### Kevin Buzzard (Aug 02 2019 at 11:25):

convert h1 fails horribly with goals like int = enat

#### Kevin Buzzard (Aug 02 2019 at 11:25):

I'm making progress though.

#### Johan Commelin (Aug 02 2019 at 11:25):

Ah, there is also `multiplicity.nat_eq_int`

or whatever.

#### Chris Hughes (Aug 02 2019 at 11:25):

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

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

#### Johan Commelin (Aug 02 2019 at 11:26):

`int.coe_nat_multiplicity`

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

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

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

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

#### Kevin Buzzard (Aug 02 2019 at 11:51):

@Paul-Nicolas Madelaine I used `norm_cast`

11 times! Thank you so much!

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

#### Johan Commelin (Aug 02 2019 at 11:53):

Ooh, wait. You already found a proof.

#### Kevin Buzzard (Aug 02 2019 at 11:53):

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

#### Kevin Buzzard (Aug 02 2019 at 11:53):

Yes, there are no sorries in the gist.

#### Kevin Buzzard (Aug 02 2019 at 11:54):

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 (Aug 02 2019 at 11:55):

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

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

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

#### 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?

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

#### 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 $\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 (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`

.

#### 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 $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 (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.

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

#### Floris van Doorn (Aug 02 2019 at 20:29):

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

#### Bryan Gin-ge Chen (Aug 02 2019 at 20:29):

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

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

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

#### Kevin Buzzard (Aug 06 2019 at 17:32):

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

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

#### Patrick Massot (Aug 06 2019 at 18:24):

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

#### Patrick Massot (Aug 06 2019 at 18:25):

For the record, Kevin:

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

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