## Stream: new members

### Topic: Maths Challenges

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

#### Mario Carneiro (Dec 09 2019 at 13:25):

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

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

#### Kevin Buzzard (Dec 09 2019 at 14:36):

And then we could have a Twitter poll

#### Kevin Buzzard (Dec 09 2019 at 14:37):

Ok next one tomorrow!

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

#### Mario Carneiro (Dec 09 2019 at 15:39):

I have a MSE question about that one

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

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

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

#### Kevin Buzzard (Dec 12 2019 at 22:37):

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

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

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

#### Johan Commelin (Dec 13 2019 at 05:59):

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

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

#### Patrick Massot (Dec 13 2019 at 09:32):

Of course you also directly write a proof term.

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

#### Kevin Buzzard (Dec 13 2019 at 09:34):

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

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

#### Patrick Massot (Dec 13 2019 at 09:34):

Am I allowed to post solutions here?

Sure

#### Kevin Buzzard (Dec 13 2019 at 09:35):

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

#### Patrick Massot (Dec 13 2019 at 09:35):

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

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

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

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

#### Etienne Laurin (Dec 18 2019 at 20:17):

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

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


#### Joe (Dec 18 2019 at 20:34):

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

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

#### Patrick Massot (Dec 18 2019 at 22:15):

Beauty is in the eye of the beholder.

#### Patrick Massot (Dec 18 2019 at 22:16):

I feel by norm_num is the only appropriate answer.

#### Rob Lewis (Dec 18 2019 at 22:17):

set_option pp.numerals false

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

#### Patrick Massot (Dec 18 2019 at 22:18):

Sure. We'll always need experts.

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

#### Kevin Buzzard (Dec 20 2019 at 07:56):

thanks, I'll fix

Last updated: May 06 2021 at 21:09 UTC