Zulip Chat Archive

Stream: new members

Topic: Maths Challenges


view this post on Zulip Kevin Buzzard (Dec 09 2019 at 12:55):

As if I didn't have too much to do already, I'm going to start running Maths challenges for the Lean curious and I'll promote it on Twitter. My understanding of Lean on Twitter is that Lean is quite a niche thing (apparently -- I must be in some kind of bubble?), but there are sufficiently many people on Twitter who are sufficiently Lean-curious that they will try the natural number game and then perhaps ask what to do next. All my answers so far have been lacking in some ways (e.g. "wait until I finish the real number game"/"wait until I finish some more levels of the natural number game"/"wait until I write the integer game"/"read Theorem Proving In Lean"/"try doing some maths on your own and get completely stuck and then ask on the chat"). On the other hand I am hoping that I will be able to knock off one relatively simple question per week (maybe I will even do a few this week, to get the ball rolling) to give beginners some experience.

I will note that I wouldn't really be able to do this without the wonderful community Lean web editor so many thanks to @Bryan Gin-ge Chen and whoever else was involved with making this tool. The official Lean web editor is simply too old now, it adds to the confusion rather than making life easier. I teach the use tactic in natnumgame and it's not in the official editor.

view this post on Zulip Mario Carneiro (Dec 09 2019 at 13:25):

How about "Advent of Proof"?

view this post on Zulip Mario Carneiro (Dec 09 2019 at 13:25):

one puzzle a day is probably a bit tough unless you have a backlog prepared though

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 14:36):

Maybe I could throw one our a day and after a few days start calling for suggestions on the chat

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 14:36):

And then we could have a Twitter poll

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 14:37):

Ok next one tomorrow!

view this post on Zulip Bhavik Mehta (Dec 09 2019 at 15:08):

I think it's a bit harder than the ones you have so far, but nat.choose n r <= nat.choose n (n/2) might be a good one (I think I'll PR this to mathlib soon as well)

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:39):

I have a MSE question about that one

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:44):

Here's a somewhat challenging one: Prove the Möbius function is multiplicative. (Easy mode: define the Möbius function)

view this post on Zulip Bhavik Mehta (Dec 09 2019 at 15:55):

I have a MSE question about that one

Yeah that's how I did it too! It's tempting to do by induction on n as well, but I haven't got that way to work yet

view this post on Zulip Jalex Stark (Dec 09 2019 at 21:36):

for what it's worth, I've been finding "do the M40001 term sheets" to be a pretty informative next step from the natural number game

view this post on Zulip Kevin Buzzard (Dec 12 2019 at 22:37):

I posted another challenge. I'll try to do a few per week.

view this post on Zulip YH (Dec 13 2019 at 00:50):

Interesting. I just did the challenge, but I have one question, if I did apply le_antisymm, and proved a ≤ b is there a way for me to say "by obvious symmetry we also have b ≤ a" instead of redo it?

view this post on Zulip Lucas Allen (Dec 13 2019 at 05:13):

I'm really enjoying these Lean problems (natural number game and maths challenges.) They're good fun and I think they're a good way to learn about some of the different parts of mathlib. Thanks for writing them Kevin Buzzard.

view this post on Zulip Johan Commelin (Dec 13 2019 at 05:59):

@YH you can try wlog a ≤ b (up to syntax errors on my side)

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:31):

What Johan meant is: wlog h : a ≤ b. That tactic is smart enough to figure out why the other case follows. You still need one more line to finish the challenge though.

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:32):

Of course you also directly write a proof term.

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 09:33):

I am still trying to work out a general framework for how I should do this. Perhaps I should collect various approaches in a solutions.lean file

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 09:34):

It's good that wlog now works in an intuitive way

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:34):

@Kevin Buzzard I just had a look at your official solution. Maybe you should warn readers that this is a very inefficient solution.

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:34):

Am I allowed to post solutions here?

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 09:34):

Sure

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 09:35):

I will perhaps collect them up and put them in the Xena GitHub repo

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:35):

The proof term is le_antisymm (ha.2 hb.1) (hb.2 ha.1) of course.

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:37):

But the lazy tactic one is: by linarith [hb.2 ha.1, ha.2 hb.1] or by { wlog h: a ≤ b, linarith [hb.2 ha.1] }.

view this post on Zulip Patrick Massot (Dec 13 2019 at 09:39):

Where linarith simply applies le_antisymm. (Do we have an emoji warning Mario not to read a message?)

view this post on Zulip Kevin Buzzard (Dec 13 2019 at 13:08):

These are great. I will figure out a way of preserving them. I think beginners who manage to figure out a method will appreciate seeing lots of others

view this post on Zulip Etienne Laurin (Dec 18 2019 at 20:17):

Is it possible to write a small proof term for challenge 3?

view this post on Zulip Joe (Dec 18 2019 at 20:30):

According to library_search, nat.bit0_ne_bit1 2 2 proves (2 + 2 : ℕ) ≠ (5 : ℕ)

example : (2 + 2 : )  (5 : ) := nat.bit0_ne_bit1 2 2

view this post on Zulip Joe (Dec 18 2019 at 20:34):

Though I guess there is no short proof of nat.bit0_ne_bit1

view this post on Zulip Rob Lewis (Dec 18 2019 at 20:34):

But Challenge 3 is over the reals, right? Try λ h, zero_ne_one $ eq.trans (eq.symm (sub_eq_zero_of_eq h.symm)) (add_sub_cancel' _ _)

view this post on Zulip Joe (Dec 18 2019 at 20:35):

Oh, that's true. My mistake.

view this post on Zulip YH (Dec 18 2019 at 20:49):

The tactic norm_num does it but I'm not sure what exactly proof term behind is.

view this post on Zulip Mario Carneiro (Dec 18 2019 at 22:06):

Basically, a linear ordered field is characteristic zero so bit0 and bit1 are injective and disjoint

view this post on Zulip Etienne Laurin (Dec 18 2019 at 22:06):

Rob thanks, that works. How do you come up with something like add_sub_cancel'? I had a hard time even understanding how a + b - a = b matched (5 - (2 + 2) = 1)

view this post on Zulip Mario Carneiro (Dec 18 2019 at 22:07):

5 unfolds to 2 + 2 + 1 by definition

view this post on Zulip Mario Carneiro (Dec 18 2019 at 22:07):

because it is bit1 2

view this post on Zulip Patrick Massot (Dec 18 2019 at 22:08):

There can be only one conclusion: we want a tactic to do that without telling us the proof term. The good part is it already exists :smiley:

view this post on Zulip Mario Carneiro (Dec 18 2019 at 22:08):

If you use specially prepared theorems, the proof is easy: bit0_ne_bit1

view this post on Zulip Mario Carneiro (Dec 18 2019 at 22:09):

that's what norm_num does

view this post on Zulip Rob Lewis (Dec 18 2019 at 22:14):

Right, the trick is knowing how numerals are defined. There are only a few important components here: 5 is defined to be (2 + 2) + 1, and the "canonical" disequality is zero_ne_one. You can combine those in various ways to prove it. Here's one without a lambda: ne.symm $ sub_ne_zero.1 $ ne_of_eq_of_ne (add_sub_cancel' _ _) one_ne_zero.

view this post on Zulip Etienne Laurin (Dec 18 2019 at 22:15):

Is there an easy way to see the bit representation? I've discovered unfold has_one.one but it doesn't seem ideal

view this post on Zulip Patrick Massot (Dec 18 2019 at 22:15):

Beauty is in the eye of the beholder.

view this post on Zulip Patrick Massot (Dec 18 2019 at 22:16):

I feel by norm_num is the only appropriate answer.

view this post on Zulip Rob Lewis (Dec 18 2019 at 22:17):

set_option pp.numerals false

view this post on Zulip Rob Lewis (Dec 18 2019 at 22:18):

I'm not sure anyone is claiming these proofs are more beautiful than norm_num. But someone had to know these proofs to implement norm_num.

view this post on Zulip Patrick Massot (Dec 18 2019 at 22:18):

Sure. We'll always need experts.

view this post on Zulip Haden Hooyeon Lee (Dec 20 2019 at 07:47):

These challenges are super helpful! Just a minor comment - the third challenge uses namespace 'challenge2' which probably should be 'challenge3' (in both challenge and solution files).

view this post on Zulip Kevin Buzzard (Dec 20 2019 at 07:56):

thanks, I'll fix


Last updated: May 06 2021 at 21:09 UTC