Maths Challenges

Stream: new members

[Kevin Buzzard]

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.

[Mario Carneiro]

How about "Advent of Proof"?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

And then we could have a Twitter poll

[Kevin Buzzard]

Ok next one tomorrow!

[Bhavik Mehta]

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)

[Mario Carneiro]

I have a MSE question about that one

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Jalex Stark]

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

[Kevin Buzzard]

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

[YH]

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?

[Lucas Allen]

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.

[Johan Commelin]

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

[Patrick Massot]

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.

[Patrick Massot]

Of course you also directly write a proof term.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

Am I allowed to post solutions here?

[Kevin Buzzard]

Sure

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Etienne Laurin]

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

[Joe]

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

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

[Joe]

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

[Rob Lewis]

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' _ _)

[Joe]

Oh, that's true. My mistake.

[YH]

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

[Mario Carneiro]

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

[Etienne Laurin]

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)

[Mario Carneiro]

5 unfolds to 2 + 2 + 1 by definition

[Mario Carneiro]

because it is bit1 2

[Patrick Massot]

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:

[Mario Carneiro]

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

[Mario Carneiro]

that's what norm_num does

[Rob Lewis]

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.

[Etienne Laurin]

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

[Patrick Massot]

Beauty is in the eye of the beholder.

[Patrick Massot]

I feel by norm_num is the only appropriate answer.

[Rob Lewis]

set_option pp.numerals false

[Rob Lewis]

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.

[Patrick Massot]

Sure. We'll always need experts.

[Haden Hooyeon Lee]

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

[Kevin Buzzard]

thanks, I'll fix