Invitation to join the Codewars Lean community, Round 1

Stream: general

[Donald Sebastian Leung]

I hereby write to you to invite you to sign up for an account on Codewars: https://www.codewars.com

Codewars is a training platform where programmers of all disciplines train on code challenges called Kata in order to improve their programming skills, and we are now extending our invitation to pure mathematicians interested in computerized theorem proving.

The Lean theorem prover was recently added to Codewars (approx. April 2020), with 11 theorem-proving challenges (3 approved, 8 still in Beta) at the time of writing. Note that Lean support on Codewars is currently in the alpha stage, i.e. it is very much experimental for now and things (e.g. challenge setup, execution time limit, etc.) may change in the near future, so we are primarily looking for (moderately) experienced Lean users interested in trying out our platform to join at this stage, i.e. if you are a beginner just started with learning Lean then you may consider joining later (e.g. on a second invitation to be determined in the near future) for an optimal experience.

Once you sign up for an account on Codewars, feel free to try out our current list of approved Lean challenges (3 at the time of writing), known as Kata on Codewars. Approved Kata are challenges that have already passed the quality-checks and scrutiny of the community and therefore should be of high quality.

But more importantly, please also consider trying out our current list of Beta Lean Kata (8 at the time of writing) if you've tried out the approved Kata and enjoyed the experience you had so far. Beta Kata are challenges contributed by the community that have yet to pass the quality-checks and scrutiny of the (rest of the) community. In order for Beta Kata to leave Beta, they have to be completed by other members of the community and receive a certain number of satisfaction votes and rank assessments.

After you've tried some of the approved and Beta Kata, given that you are satisfied with the overall experience, please do consider authoring Lean Kata of your own to contribute back to the community. This could be something simple like an extension to one of the levels in the NNG or something more challenging such as proving that all Lipschitz functions are uniformly continuous (or even perhaps landmark results in complex analysis (for example)!). Your Kata will then pass through the Beta phase and (hopefully) eventually get approved as with every other Kata.

To learn more about the Lean environment on Codewars, please refer to the Wiki entry. You can also learn more about the Beta Process here. And last but not least, feel free to drop by the Codewars Gitter chat if you have any questions or would just like to discuss about Codewars in general.

---

For more computer-science oriented Lean users, you may be delighted to know that Codewars also supports Coq, Idris and Agda (support is pretty much stable) as well, with over 40 approved Kata and 20 Beta Kata spanning topics in discrete mathematics, programming language theory, verified functional algorithms ... If you see a (Coq / Idris / Agda) Kata that you would fancy being made available in Lean as well, feel free to leave a comment on the Kata concerned and we'll see which ones we can make available in Lean. Alternatively, if you happen to do Coq / Idris / Agda as well then feel free to (first) complete said Kata in one of those languages and submit a Lean translation to the Kata author, which, once approved, will make the Kata available in Lean for everyone :smile:

[Kevin Buzzard]

@Donald Sebastian Leung can I use mathlib in my solution somehow?

[Kevin Buzzard]

I literally don't know where to start with the kata I'm working on without mathlib

[Kevin Buzzard]

OK so (a) you can use mathlib [I just added the imports to the submission file] and (b) I just solved the first kata :-) I am now 7 kyu at Lean :P

[Donald Sebastian Leung]

Kevin Buzzard said:

Donald Sebastian Leung can I use mathlib in my solution somehow?

Kevin Buzzard said:

I literally don't know where to start with the kata I'm working on without mathlib

Sorry for the confusion. Would it help if I mention mathlib as one of the installed packages in the Wiki page?

[Kevin Buzzard]

I didn't look at any wiki pages, I just got going. Maybe it's a good idea. Sometimes mathlib comes as standard and sometimes it doesn't -- see for example the community web editor v the official one

[Reid Barton]

Probably a good idea to mention the specific version (git commit id) of mathlib installed somewhere though, since it won't always be the current one

[Kevin Buzzard]

Donald kindly added two number theory Kata which I suggested; they are currently in beta but you can still submit solutions. One of them is probably harder than the three non-beta kata. Note that no discussion of the problems should occur here; you can only see the full discussion about a problems once you've solved it on the site.

[Johan Commelin]

So, I've played a bit on the site. But currently you cannot have the interactive goal state as far as I can see.

[Johan Commelin]

@Donald Sebastian Leung First I should say: "Wow, that site looks really cool. Thanks for adding Lean!"

[Johan Commelin]

But, how are you supposed to do the Lean problems? Copy-paste to VScode? Or did I miss some button to get a "Lean IDE" online?

[Kevin Buzzard]

You copy paste. No online IDE.

[Donald Sebastian Leung]

Unfortunately, we do not support interactive proof editing (same for Coq / Idris / Agda); the expected way to solve a Kata is by developing your solution locally and submitting it onto the site when you're done :sweat_smile: You may learn more about our Lean setup on the Wiki page.

[Kevin Buzzard]

And they're currently in the process of telling us what mathlib commit they're using :-)and the mathlib commit they use is at the bottom of the Wiki page (it's from 29th March)

[Kenny Lau]

[Kenny Lau]

?????

[Kevin Buzzard]

https://github.com/codewars/codewars.com/issues/2087

[Johan Commelin]

@Donald Sebastian Leung wasn't it discovered by Kenny?

[Kevin Buzzard]

Independently ;-)

[Kevin Buzzard]

It's probably not a coincidence that if you basically do all the Lean Kata right now then you get over 75 but under 300 rep points :-)

[Johan Commelin]

Aah... so now we'll have eternal debates about whether this is the Lau bug or the Buzzard bug or the Buzzard–Lau bug, etc...

[Kevin Buzzard]

Kenny is still junior so I think it should be named the Lau bug.

[Reid Barton]

Or at least the Lau-Buzzard bug: fight the alphabetical bias!

[Kenny Lau]

Kevin Buzzard said:

It's probably not a coincidence that if you basically do all the Lean Kata right now then you get over 75 but under 300 rep points :-)

I've finished (and voted on) all 13 outstanding kata and I now have 96 honour

[Kenny Lau]

I invite y'all to do my new kata: https://www.codewars.com/kata/5e8b9787c2eb9f0029aa73a0

[Kenny Lau]

and this new kata co-authored with kbuzzard: https://www.codewars.com/kata/5e8c4b4a968b34002d4b6534/lean

[Donald Sebastian Leung]

Let's vote (:+1: if you are interested, :-1: otherwise): who would like to see Times Three, Plus Five available in Lean?

[Donald Sebastian Leung]

And Exponentiation by squaring

[Donald Sebastian Leung]

And Fast Fibonacci numbers

[Donald Sebastian Leung]

(I initially did not consider translating them into Lean since they were about "program verification", but these particular ones could also be reasonably viewed as math problems IMO)

[Kevin Buzzard]

These all look like mathematics, in some sense. Kenny's kata is of a similar nature to these. Our joint kata about units in rings is mathematics of a different nature (and probably much harder) but my gut feeling right now is to get as many kata into the system and then promote it.

[Kevin Buzzard]

I agree that these questions are very "computer-sciency" in some sense, but basic mathematical kata on things like sets and functions will appear at some point.

[Patrick Massot]

The issue with interesting elementary problems is the solution will be in mathlib...

[Kevin Buzzard]

I see -- so they need to be "recreational" in some sense.

[Patrick Massot]

I guess so.

[Kevin Buzzard]

I have a bunch of training material for olympiad people, I guess it might be interesting to turn some of those into kata.

[Alex J. Best]

I guess the question should be what the goal of kata are? To teach people lean fundamentals (with a kata teaching various tricks / techniques) or more general practice at lean without specific lessons in mind or just fun math problems for people who know some lean?

[Kevin Buzzard]

I think it should just be all of the above. I don't think it's possible to look at the gazillion python kata on Codewars and say "now what is generally the point of these kata?". They have many many points.

[Mario Carneiro]

I don't see why there is or should be a bias against "computer-sciency" lean kata

[Mario Carneiro]

That is, I don't understand

I initially did not consider translating them into Lean since they were about "program verification"

[Kenny Lau]

do we have any metaprogramming kata in any theorem prover?

[Johan Commelin]

How many theorem provers support metaprogramming?

[Kenny Lau]

Lean is the only theorem prover I know

[Johan Commelin]

Then the answer is probably 0

[Kenny Lau]

then maybe we can have metaprogramming kata for Lean anyways

[Mario Carneiro]

All the HOL family provers have extensive metaprogramming capabilities, because it's more like a theorem prover in an interactive shell than a programming language in a theorem prover

[Donald Sebastian Leung]

Well, in Coq, we do have Ltac practice: The tarai function. Metaprogramming is not absolutely required in the Kata, but certainly makes your life much easier (which is also the point of the Kata).

[Donald Sebastian Leung]

By the way, I saw that some of you have started translating some existing Kata into Lean :+1: In case:

• the Kata author has been inactive for at least a month (e.g. since it's now April 2020, the author is definitely inactive for at least a month if (s)he is last seen on Feb 2020 or earlier), OR
• your translation is at least a week old,

then feel free to post the link to said translation here (please also mention which Kata it is for) and I can approve them instead. Cheers :smile:

[Kenny Lau]

I can't find any new Lean kata?

[Donald Sebastian Leung]

Not yet - I've been busy completing online midterms today (a complete disaster :sad: ) so I haven't had the time to translate existing Kata into Lean. But, if you wish, you could browse through the list of available Coq Kata (or even Idris / Agda Kata) and see which ones you would like available in Lean and either 1) notify me (on this thread or otherwise) and I can see which ones I am able to translate into Lean, or 2) forfeit them in Coq ( / Idris / Agda) and write / submit your own Lean translation.

[Kevin Buzzard]

I think that independent of translating Kata we should be also thinking of cute little maths problems, of all levels, and formalising them. There is essentially no risk of them being duplicates as far as I can see, because most languages on the site do not support proofs, and those that do seem to have Kata which are mostly on the programming side

[Kenny Lau]

@Donald Sebastian Leung how do I send you the translation without giving the solution away?

[Donald Sebastian Leung]

@Kenny Lau I assume you mean the link to your published translation? The answer is: you can't. If I click on the link to view the translation then I can see the changes you made to the description, the Preloaded section, Initial / Complete Solution and Sample / Submit tests immediately, since (ideally) I have to review the translation before approving / rejecting it. Of course, once I click on the link to view the translation, I immediately forfeit the Kata, at least in the language of the translation and IIRC also in all other languages as well (that's why I asked everyone to mention which Kata it is for when posting links to translations).

[Kenny Lau]

I translated this kata into Lean: https://www.codewars.com/kata/514b92a657cdc65150000006/python

[Kenny Lau]

Following advice from D. S. Leung, I have instead authored a new kata: https://www.codewars.com/kata/5e8dccdb8a011a0028a3f5f8

[Kenny Lau]

Another collab with Buzzard: every group of order 4 is commutative

[Johan Commelin]

That out to be just dec_trivial, right? </joking>

[Johan Commelin]

I guess that running through $4^{16}$ binary ops is a bit inefficient...

[Kevin Buzzard]

You also need a transfer tactic

[Kevin Buzzard]

4^16 only does groups up to isomorphism

[Kenny Lau]

The kata Fermat was wrong by D. S. Leung got approved.

[Kenny Lau]

Does anyone know what it takes for a kata to be approved?

[Kevin Buzzard]

IIRC this is documented on the Wiki

[Kevin Buzzard]

It's slightly complex -- IIRC you need a certain amount of positivity from a certain number of people, but the more rep you have the more positivity you can give

[Kenny Lau]

I have written a new kata: Order-preserving bijection from rationals to non-zero rationals

[Kenny Lau]

We now have 4 approved kata and 14 beta kata in Lean

[Kenny Lau]

What does it mean here that at 6000 honour one can "approve a beta kata and assign its rank"?

[Donald Sebastian Leung]

This means that, given that you have 6k+ honor, if you see a Beta Kata whose status is "Awaiting moderator approval", you can go in and edit the Kata, set its rank using a dropdown, and click "Re-Publish" which changes it from a Beta Kata into an approved one, much like what happened recently with the "Fermat was wrong" Kata :smile:

[Reid Barton]

Sounds like an infinite honour exploit to me

[Reid Barton]

I guess that would be dishonourable, though.

[Donald Sebastian Leung]

Well, of course you're expected to use your moderating powers responsibly :wink: There has been at least one incident where a moderator had his / her Kata-approving privileges temporarily revoked for abusing it

[Donald Sebastian Leung]

(But for that particular case, it turned out that the moderator concerned meant no harm and simply misinterpreted the message for Kata approval in some way. (S)he promised to act responsibly and his / her privileges were swiftly restored.)

[Kevin Buzzard]

How many people have 6k+ honor?

[Donald Sebastian Leung]

At least 500

[Donald Sebastian Leung]

I've been bugging my fellow moderators to approve Lean translations for the following 5 Kata (all over a week old), so hopefully they will be available in Lean pretty soon:

• A + A = B + B so A = B? Prove it!
• This square is perfect
• Drinker paradox
• Squared triangular numbers
• Magic is Commutative

I have also been busy working on a translation to Times 3, Plus 5 lately but I've been bogged down by homework lately so apologies for the delay. Though I expect I should be able to complete the translation tonight.

[Kenny Lau]

Why is this Agda kata "List concatenation is injective? Prove it!" 1 kyu?

[Donald Sebastian Leung]

@Kevin Buzzard would you mind doing me a favor and telling Kenny "the story"? :wink:

[Donald Sebastian Leung]

@Kenny Lau Yes, it's severely overranked, it should be at most 5 kyu

[Donald Sebastian Leung]

BTW, see https://github.com/codewars/codewars.com/issues/2030 (and please upvote it) :smile:

[Donald Sebastian Leung]

I have also been busy working on a translation to Times 3, Plus 5 lately but I've been bogged down by homework lately so apologies for the delay. Though I expect I should be able to complete the translation tonight.

Okay, this might have to wait till tomorrow, I've been busy wrestling with Lean but I need to go to sleep now. Goodnight! :zzz:

[Kenny Lau]

Hopefully this easy kata will be more popular: Show that there are two types that are unequal

[Kevin Buzzard]

we are primarily looking for (moderately) experienced Lean users interested in trying out our platform to join at this stage, i.e. if you are a beginner just started with learning Lean then you may consider joining later (e.g. on a second invitation to be determined in the near future) for an optimal experience.

I was waiting for Donald to give us the go-ahead before I started banging on about it on social media.

[Kenny Lau]

I don't think the current experience would be optimal because of the sever deficit in the number of (un)approved kata

[Kenny Lau]

by "popular" I mean popular within the pioneers such as you

[Kevin Buzzard]

Right, that's why I'm not banging on about it on social media

[Kenny Lau]

@Simon Hudon created a tactical solution to Fermat was wrong, which has 11 solutions; also, Multiples of 3, you say? has 8 solutions

[Kenny Lau]

so there are definitely people who are interested

[Kevin Buzzard]

wooah did Simon write his own primality tester in his solution? :-)

[Simon Hudon]

Haha! No, it's already in data.nat.primes

[Kenny Lau]

you cheated by starting with 3 though :-)

[Kenny Lau]

Let's settle it once and for all: is it Kata or is it kata?

[Kevin Buzzard]

He could have started with [integer removed due to no spoiler policy] like some of the others :-)

[Kevin Buzzard]

Oh this is great, a bunch of people have done a bunch of Kata. It would be good to get some of these out of beta.

[Kenny Lau]

New kata cowritten with Buzzard: Prove that this sequence contains only integers

[Reid Barton]

The kata description is wrong (- instead of +)

[Reid Barton]

Also, I was hoping it was a Somos sequence and ... I'm not sure whether it is one.

[Kenny Lau]

thanks, corrected

[Donald Sebastian Leung]

Kenny Lau said:

Let's settle it once and for all: is it Kata or is it kata?

:+1: for Kata; :-1: for kata

[Donald Sebastian Leung]

Donald Sebastian Leung said:

I've been bugging my fellow moderators to approve Lean translations for the following 5 Kata (all over a week old), so hopefully they will be available in Lean pretty soon:

• A + A = B + B so A = B? Prove it!
• This square is perfect
• Drinker paradox
• Squared triangular numbers
• Magic is Commutative

I have also been busy working on a translation to Times 3, Plus 5 lately but I've been bogged down by homework lately so apologies for the delay. Though I expect I should be able to complete the translation tonight.

Still bugging my fellow moderators to approve them, but one of them said that the one for "A + A = B + B" should be rejected (and frankly I agree with him) since it's too easy in Lean even for 6 kyu

On the other hand, good news: a respectable Codewarrior has just declared his interest in learning Lean so he might start contributing to Lean development on Codewars in the near future

[Kenny Lau]

Can a translation have a different rank?

[Donald Sebastian Leung]

No, rank is per-kata

[Donald Sebastian Leung]

But it has been suggested before to have separate ranks for each translation

[Donald Sebastian Leung]

Lemme try to find the related GitHub issue ...

[Kenny Lau]

A translation of a Coq kata: A random fact about filtering

[Kenny Lau]

hey maybe this is the best way to get approved Lean kata

[Kenny Lau]

A translation of a Coq kata: Real Fibonacci

[Kenny Lau]

This reminds me of the movie Parasite.

[Markus Himmel]

I also made a kata: every group action of a group of order 65 on a set with 27 elements has a fixed point.

[Kenny Lau]

@Mario Carneiro looks like this kata reveals some holes in the theory of group actions in mathlib (the details are omitted because no spoilers)

[Kenny Lau]

@Markus Himmel how on earth did your solution manage to stay below the time limit

[Kenny Lau]

I'm not even halfway through mine and it's already frustratingly slow

[Kenny Lau]

@Markus Himmel I have stated an issue in the kata discourse.

[Markus Himmel]

Kenny Lau said:

Markus Himmel how on earth did your solution manage to stay below the time limit

I had to optimize my solution quite a bit. It would be nice to set the time limit to a minute or something.

[Mario Carneiro]

I'm glad there is a time limit, it adds an extra dimension to the challenge

[Kevin Buzzard]

Yeah, it means I can't do my own kata about there being no commutative ring with 5 units :-)

[Kenny Lau]

Mario Carneiro said:

I'm glad there is a time limit, it adds an extra dimension to the challenge

not if the bottleneck is parsing took 22.8s

[Markus Himmel]

I think it's fine to have a time limit, but it should be adjustable.

[Mario Carneiro]

it can't be too adjustable or else it could be a DDOS issue

[Kevin Buzzard]

millions of fake Lean users all trying to prove that there are no commutative rings with 5 units

[Mario Carneiro]

maybe it's a polymath project

[Donald Sebastian Leung]

Markus Himmel said:

I think it's fine to have a time limit, but it should be adjustable.

Feel free to leave your suggestion(s) and / or upvote Codewars/codewars-runner-cli#803

[Kenny Lau]

Lean translation Electric Boogaloo: Empty Place in a Binary Tree

[Kenny Lau]

Markus Himmel said:

I also made a kata: every group action of a group of order 65 on a set with 27 elements has a fixed point.

I finally managed to optimize my solution enough: 12396ms

[Mario Carneiro]

The description for "empty place" is still written in Coq?

[Mario Carneiro]

also the terminology makes no sense

[Markus Himmel]

A relatively easy kata about category theory: Pushouts and epimorphisms

[Reid Barton]

it should be a mathlib pr instead, though!

[Kevin Buzzard]

I'm afraid we can't have this result in mathlib now, it would be a spoiler

[Markus Himmel]

Huh. This is an exercise in Mac Lane and it looked useless enough so I thought it might be a cool kata which will never find its way into mathlib, but now I looked it up in Borceux and he writes "The following result is obvious, but will prove to have interesting consequences" and he uses it at least five times in the rest of volume 1 of his handbook. So I guess this really will be a mathlib PR at some point. On the other hand, this is so easy that I don't think it would be a problem for the kata if the answer was in mathlib.

[Kevin Buzzard]

I am not being serious. I'm sure it's both a great kata and a great PR.

[Markus Himmel]

I know, I was just surprised that there is more to the result than I thought.

[Kevin Buzzard]

In category theory in Lean there is always more to it than you thought :-)

[Kenny Lau]

More plasmodium: Program Verification #3: Tail-recursive sum

[Kenny Lau]

Markus Himmel said:

A relatively easy kata about category theory: Pushouts and epimorphisms

hmm, our solutions are very similar

[Bhavik Mehta]

Reid Barton said:

it should be a mathlib pr instead, though!

If anyone is planning to do this, we have the dual results here which could save someone some time

[Donald Sebastian Leung]

So I just checked and we have over 30 Lean Kata on Codewars, thank you to all who actively participated in pushing new content to the site :tada: What do you all think about starting the second round of invitations now?

:+1: for yes, :-1: for not yet

[Kenny Lau]

Paradoxically, we need to encourage people here to learn Coq/Agda/Idris to build more parasites

[Donald Sebastian Leung]

Donald Sebastian Leung said:

So I just checked and we have over 30 Lean Kata on Codewars, thank you to all who actively participated in pushing new content to the site :tada: What do you all think about starting the second round of invitations now?

:+1: for yes, :-1: for not yet

@Kevin Buzzard What do you think?

[Kevin Buzzard]

I have no experience in these matters. Oh but there are now 11 out of beta? That seems like a far more respectable amount than 3 :-)

[Donald Sebastian Leung]

So I'll take that as a "yes"? :smile:

IMO it does not really matter if most of Lean kata are currently in Beta. As long as we remind fellow Codewarriors to leave their satisfaction votes and rank assessments on every beta kata they complete then we should have many more approved Lean kata very soon.

[Kenny Lau]

The kata in Coq limbo really terrify me