## 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: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,
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,
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,
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 (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 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,
norm_cast,
all_goals {rw [mul_comm, nat.mul_div_cancel], exact dec_trivial},
},
{ rw hn,
norm_cast,
}
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 h,
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,
intro h,
have := hm (m / 2) _ _,
norm_cast,
exact easy m,
rw nat.div_lt_iff_lt_mul',
rw mul_two,
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!)) 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: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:

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