Zulip Chat Archive

Stream: general

Topic: Invitation to join the Codewars Lean community, Round 1


view this post on Zulip Donald Sebastian Leung (Apr 04 2020 at 16:13):

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:

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 17:04):

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 17:05):

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

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 17:55):

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

view this post on Zulip Donald Sebastian Leung (Apr 05 2020 at 05:51):

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?

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 08:32):

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

view this post on Zulip Reid Barton (Apr 05 2020 at 12:55):

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

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 10:05):

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.

view this post on Zulip Johan Commelin (Apr 06 2020 at 10:07):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 10:07):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 10:08):

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?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 10:12):

You copy paste. No online IDE.

view this post on Zulip Donald Sebastian Leung (Apr 06 2020 at 10:12):

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.

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 10:13):

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)

view this post on Zulip Kenny Lau (Apr 06 2020 at 12:23):

view this post on Zulip Kenny Lau (Apr 06 2020 at 12:23):

?????

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 12:35):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 12:41):

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

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 12:41):

Independently ;-)

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 12:42):

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

view this post on Zulip Johan Commelin (Apr 06 2020 at 12:42):

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

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 12:44):

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

view this post on Zulip Reid Barton (Apr 06 2020 at 12:47):

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

view this post on Zulip Kenny Lau (Apr 06 2020 at 13:02):

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

view this post on Zulip Kenny Lau (Apr 07 2020 at 05:15):

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

view this post on Zulip Kenny Lau (Apr 07 2020 at 09:48):

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

view this post on Zulip Donald Sebastian Leung (Apr 07 2020 at 12:16):

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

view this post on Zulip Donald Sebastian Leung (Apr 07 2020 at 12:17):

And Exponentiation by squaring

view this post on Zulip Donald Sebastian Leung (Apr 07 2020 at 12:17):

And Fast Fibonacci numbers

view this post on Zulip Donald Sebastian Leung (Apr 07 2020 at 12:19):

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

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 12:24):

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.

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 12:38):

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.

view this post on Zulip Patrick Massot (Apr 07 2020 at 12:39):

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

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 12:40):

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

view this post on Zulip Patrick Massot (Apr 07 2020 at 12:40):

I guess so.

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 12:41):

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

view this post on Zulip Alex J. Best (Apr 07 2020 at 12:46):

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?

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 12:50):

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.

view this post on Zulip Mario Carneiro (Apr 07 2020 at 21:26):

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

view this post on Zulip Mario Carneiro (Apr 07 2020 at 21:27):

That is, I don't understand

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 05:18):

do we have any metaprogramming kata in any theorem prover?

view this post on Zulip Johan Commelin (Apr 08 2020 at 05:18):

How many theorem provers support metaprogramming?

view this post on Zulip Kenny Lau (Apr 08 2020 at 05:19):

Lean is the only theorem prover I know

view this post on Zulip Johan Commelin (Apr 08 2020 at 05:23):

Then the answer is probably 0

view this post on Zulip Kenny Lau (Apr 08 2020 at 05:24):

then maybe we can have metaprogramming kata for Lean anyways

view this post on Zulip Mario Carneiro (Apr 08 2020 at 06:04):

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

view this post on Zulip Donald Sebastian Leung (Apr 08 2020 at 09:13):

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

view this post on Zulip Donald Sebastian Leung (Apr 08 2020 at 10:25):

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:

view this post on Zulip Kenny Lau (Apr 08 2020 at 10:27):

I can't find any new Lean kata?

view this post on Zulip Donald Sebastian Leung (Apr 08 2020 at 10:34):

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.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 10:48):

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 11:47):

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

view this post on Zulip Donald Sebastian Leung (Apr 08 2020 at 12:22):

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 12:24):

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

view this post on Zulip Kenny Lau (Apr 08 2020 at 13:10):

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

view this post on Zulip Kenny Lau (Apr 09 2020 at 05:37):

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

view this post on Zulip Johan Commelin (Apr 09 2020 at 05:41):

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

view this post on Zulip Johan Commelin (Apr 09 2020 at 05:42):

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

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 06:38):

You also need a transfer tactic

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 06:39):

4^16 only does groups up to isomorphism

view this post on Zulip Kenny Lau (Apr 09 2020 at 12:44):

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

view this post on Zulip Kenny Lau (Apr 09 2020 at 12:44):

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

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 12:48):

IIRC this is documented on the Wiki

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 12:48):

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

view this post on Zulip Kenny Lau (Apr 09 2020 at 13:30):

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

view this post on Zulip Kenny Lau (Apr 09 2020 at 13:33):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 11:09):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 14:00):

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:

view this post on Zulip Reid Barton (Apr 10 2020 at 14:00):

Sounds like an infinite honour exploit to me

view this post on Zulip Reid Barton (Apr 10 2020 at 14:01):

I guess that would be dishonourable, though.

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 14:01):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 14:03):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 14:05):

How many people have 6k+ honor?

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 14:08):

At least 500

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 15:03):

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:

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.

view this post on Zulip Kenny Lau (Apr 10 2020 at 15:06):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 15:07):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 15:07):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 15:08):

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

view this post on Zulip Donald Sebastian Leung (Apr 10 2020 at 16:14):

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:

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:06):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 19:09):

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.

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:10):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:11):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 19:15):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:17):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:17):

so there are definitely people who are interested

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 19:44):

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

view this post on Zulip Simon Hudon (Apr 10 2020 at 19:51):

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

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:52):

you cheated by starting with 3 though :-)

view this post on Zulip Kenny Lau (Apr 10 2020 at 19:58):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 19:58):

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

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 20:00):

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.

view this post on Zulip Kenny Lau (Apr 10 2020 at 21:05):

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

view this post on Zulip Reid Barton (Apr 11 2020 at 01:18):

The kata description is wrong (- instead of +)

view this post on Zulip Reid Barton (Apr 11 2020 at 01:18):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 03:18):

thanks, corrected

view this post on Zulip Donald Sebastian Leung (Apr 11 2020 at 05:10):

Kenny Lau said:

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

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

view this post on Zulip Donald Sebastian Leung (Apr 11 2020 at 05:21):

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:

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 05:22):

Can a translation have a different rank?

view this post on Zulip Donald Sebastian Leung (Apr 11 2020 at 05:23):

No, rank is per-kata

view this post on Zulip Donald Sebastian Leung (Apr 11 2020 at 05:23):

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

view this post on Zulip Donald Sebastian Leung (Apr 11 2020 at 05:23):

Lemme try to find the related GitHub issue ...

view this post on Zulip Kenny Lau (Apr 11 2020 at 12:24):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 12:25):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 04:18):

A translation of a Coq kata: Real Fibonacci

view this post on Zulip Kenny Lau (Apr 12 2020 at 04:22):

This reminds me of the movie Parasite.

view this post on Zulip Markus Himmel (Apr 12 2020 at 06:21):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 06:40):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 07:56):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 07:56):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:29):

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 08:35):

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.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:38):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:38):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:39):

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 08:39):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:43):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:44):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:45):

maybe it's a polymath project

view this post on Zulip Donald Sebastian Leung (Apr 12 2020 at 08:49):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 10:36):

Lean translation Electric Boogaloo: Empty Place in a Binary Tree

view this post on Zulip Kenny Lau (Apr 12 2020 at 10:37):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 10:38):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 10:38):

also the terminology makes no sense

view this post on Zulip Markus Himmel (Apr 12 2020 at 14:44):

A relatively easy kata about category theory: Pushouts and epimorphisms

view this post on Zulip Reid Barton (Apr 12 2020 at 14:54):

it should be a mathlib pr instead, though!

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 14:57):

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 15:09):

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.

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 15:10):

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 15:13):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 15:32):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 18:28):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 19:02):

Markus Himmel said:

A relatively easy kata about category theory: Pushouts and epimorphisms

hmm, our solutions are very similar

view this post on Zulip Bhavik Mehta (Apr 12 2020 at 23:10):

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

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 10:20):

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

view this post on Zulip Kenny Lau (Apr 13 2020 at 10:23):

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

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 14:12):

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?

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 14:14):

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

view this post on Zulip Donald Sebastian Leung (Apr 13 2020 at 14:16):

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.

view this post on Zulip Kenny Lau (Apr 13 2020 at 14:25):

The kata in Coq limbo really terrify me


Last updated: May 17 2021 at 22:15 UTC