Invitation to join the Codewars Lean community, Round 2

Stream: general

[Donald Sebastian Leung]

I hereby invite you to sign up for an account on Codewars.

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 Lean users of all levels (whether beginner, intermediate or expert) and disciplines (mathematicians and computer scientists alike) interested in computerized theorem proving.

Lean support has been recently added to Codewars (late March / early April) and is now in the Beta Phase - we now have much more content compared to when we just started thanks to all of those who actively participated in the Round 1 invitation and generously contributed Lean kata to our site, but we are still looking forward to potential feedback on how the experience on Codewars can be improved (for Lean).

In terms of Lean challenges, we now have 11 approved kata and 20 beta kata spanning topics on synthetic geometry, category theory, number theory, abstract algebra ... and more! Feel free to browse through the list of available challenges and train on whatever challenge you find of interest. Once you have 25 honor (a scoring system on Codewars), you will also be able to vote on Kata you have completed based on how satisfied you were with the experience, so don't forget to cast your votes! :smile:

You may learn more about the Lean setup used on Codewars on our Wiki, as well as the scoring system, user privileges and the beta process. You may also wish to drop by our Gitter chat if you have any questions about Codewars or would just like to chat in general.

Happy sparring! :grinning_face_with_smiling_eyes:

[Kenny Lau]

Plasmodium: Program Verification #5: The sum of a geometric progression

[Kenny Lau]

How does beta work? More specifically, how many votes does a beta kata need to get before begin approved?

[Donald Sebastian Leung]

Generally, the number of satisfaction votes, rank assessments as well as the satisfaction rating required for a Beta kata to leave Beta decreases as 1) the average assessed rank of the kata is higher and 2) you get more and more kata approved. For example, if you currently have < 10 approved kata and the average assessed rank of your Beta kata is in the 7-8 kyu range then it will require 12 (satisfaction + ranking) votes with a satisfaction rating of >= 80% in order to be eligible to leave Beta, but if its average assessed rank is 1-2 kyu then it only requires 5 votes and >= 70% satisfaction to leave Beta.

You may learn more about the Beta Process on our Wiki; specifically, the kata approval requirements.

[Bhavik Mehta]

Is there a template for making new lean kata? For instance, how do I make sure the user didn't use any new axioms or sorry?

[Kevin Buzzard]

In about 30 minutes I was going to ask exactly the same question. I've seen this issue several times in the discussions -- "don't do it like that, it's trivial to hack" :-/

[Kevin Buzzard]

OK so I am faced with having to supply 5 files:
Complete solution
Initial solution
Preloaded
Test cases
Example test cases

[Kevin Buzzard]

Say my kata is to prove theorem easy : 2 + 2 = 4. What now? Where does all this SUBMISSION go?

[orlando]

sorry, :D

[orlando]

oups i post in a bas section sorry :D

[Kevin Buzzard]

Final Solution is invalid. (lean) The solution should pass the provided test cases What did I do wrong?

[Kevin Buzzard]

I might have got it working: elliptic curve question

[Shing Tak Lam]

Kevin Buzzard said:

Say my kata is to prove theorem easy : 2 + 2 = 4. What now? Where does all this SUBMISSION go?

I think the way that some kata have done it is to have this in your tests

import Preloaded Solution

theorem easy' : 2 + 2 = 4 := easy
#print axioms easy'

[Shing Tak Lam]

So do this instead of using SUBMISSION

[Kevin Buzzard]

For @Bhavik Mehta : the 5 Lean files I made are:
1) Complete solution: a bunch of working Lean 3.7.2 code containing theorem zany_name : my_statement := <proof>
2) Initial solution:

import Preloaded

-- some comments
theorem zany_name : my_statement := sorry

3) Preloaded:

import imports-needed-to-make-theorem-statement-compile

def SUBMISSION := my_statement
notation `SUBMISSION` := SUBMISSION

4) Test cases:

import Preloaded Solution

theorem submission : SUBMISSION := zany_name
#print axioms submission

5) Example test cases: same as test cases.

As an example: in the 5^5^5^5^5 question, zany_name is fivefives and my_statement is ¬ nat.prime ((5^5^5^5^5-1)/(5^5^(5^5^5-1)-1))

[Kevin Buzzard]

@Shing Tak Lam does my kata look OK (I'm not asking about the maths, I'm just asking if I've made any dumb errors)

[Shing Tak Lam]

I think so? At least from comparing it to existing kata.

[Shing Tak Lam]

I mean if you put it into Codewars, the preloaded.lean should fail the tests and the completed solution should pass. So if that's the case then you're probably fine? Probably best to ask someone who actually knows this stuff (Donald)

[Kevin Buzzard]

I just had a weird time uploading it; the first time it seemed to fail, and then the second time it seemed to pass instantly.

[Shing Tak Lam]

Sometimes the Codewars servers does that. It seems to depend on the load the servers are under (the time of day)...

[Mario Carneiro]

I like the good test coverage :)

[Donald Sebastian Leung]

Kevin Buzzard said:

I might have got it working: elliptic curve question

@Kevin Buzzard Congrats on authoring your first kata on the site (as yourself)! :tada:

Shing Tak Lam said:

I mean if you put it into Codewars, the preloaded.lean should fail the tests and the completed solution should pass. So if that's the case then you're probably fine? Probably best to ask someone who actually knows this stuff (Donald)

That sounds about right, except that the initial solution should only fail the tests because of a wrong input (or in the case of Lean, a sorry) and not because of a compilation error. We don't want the solver to perform unnecessary debugging just to get their solution to compile. There are exceptions where the initial solution is designed to not compile (e.g. in a weird C++ kata involving compile-time metaprogramming) but those are extremely rare.

[Donald Sebastian Leung]

Kevin Buzzard said:

I just had a weird time uploading it; the first time it seemed to fail, and then the second time it seemed to pass instantly.

Not sure if it's related here but I should probably mention this: there is a known long-standing bug on Codewars that when you publish your kata for the first time, the servers do not actually check if your kata is completable so can actually publish a broken kata that no one can possibly solve. But on every re-publish, the servers do the checking and prevents you from re-publishing if the kata becomes un-completable. The best way to ensure that you do not accidentally publish a broken kata is by clicking "Validate Solution" and making sure that the test output is green before publishing your kata.

[Donald Sebastian Leung]

Mario Carneiro said:

I like the good test coverage :)

IMO the two good things about authoring theorem-proving kata (as opposed to ordinary programming kata) on Codewars is 1) authoring a theorem-proving kata takes about the same effort as solving one, whereas authoring a programming kata requires substantially more effort in designing suitable fixed, edge and random tests and 2) the community generally give more favorable votes to theorem-proving kata (if only because there currently aren't that many and everyone wants to see more on the site), whereas, when authoring a programming kata, if you don't get it just right then you immediately get cyber-bullied shouted on by the community for all sorts of various issues and receive a flood of "Not Satisfied" votes (which could automatically retire your Beta kata, rendering it impossible to leave Beta).

[Donald Sebastian Leung]

Congrats @Kenny Lau on your first approved kata: Show that there are two types that are unequal :tada:

[Donald Sebastian Leung]

Congrats @Bhavik Mehta on your first approved kata: Every symmetric transitive relation is reflexive ... right? :tada:

And ... we now have 4 new kata on limits of sequences, check them out :wink:

[Donald Sebastian Leung]

... which brings us up to 41 (Lean) kata in total

[Patrick Massot]

Math rendering at https://www.codewars.com/kata/5e997f77ea84170016600045 is painful to see. It brings back memories of the 90's.

[Patrick Massot]

Why ∀ ε > 0, ∃ (N : ℝ), ∀ n : ℕ, ↑n > N → abs (x n - l) < ε? Why would you want to ask N to be real??

[Donald Sebastian Leung]

Patrick Massot said:

Math rendering at https://www.codewars.com/kata/5e997f77ea84170016600045 is painful to see. It brings back memories of the 90's.

Yeah, sorry about that, I don't think Codewars supports TeX / MathJAX or similar so I had to typeset the LaTeX in an external editor, take screenshots of the rendered output, upload them onto imgur and paste the images there.

There might be a way to get rid of that white background by using SVGs but I'm not all too familiar with it.

[Donald Sebastian Leung]

Patrick Massot said:

Why ∀ ε > 0, ∃ (N : ℝ), ∀ n : ℕ, ↑n > N → abs (x n - l) < ε? Why would you want to ask N to be real??

IMO it's easier to allow N to be real since otherwise one may have to round their value of N up to the nearest natural number in Lean after finding it by manipulating the inequality abs (x n - l) < ε on paper. But I am definitely no expert in analysis / Lean so feel free to leave your suggestions in the discourse of the kata concerned and I'll see if I can implement your suggestions in my spare time.

[Patrick Massot]

I strongly suggest this is a very bad idea.

[Patrick Massot]

And I've written dozens of "Katas" for my students on this topic of limits of sequences.

[Patrick Massot]

Although I haven't tried to replace the word exercise with kata.

[Patrick Massot]

It's true you can meet coercion hell with applying this definition on concrete sequence like $n \mapsto 1/n$. But what you do is enforcing coercion hell everywhere.

[Donald Sebastian Leung]

Patrick Massot said:

It's true you can meet coercion hell with applying this definition on concrete sequence like $n \mapsto 1/n$. But what you do is enforcing coercion hell everywhere.

Thanks for your input, I have made a note to myself to fix this when I get around to it.

[Donald Sebastian Leung]

Here's one on matrices (specifically, special linear groups): A special set of matrices with unique representation

And one on modular arithmetic: Times Three, Plus Five (hint: interval_cases will definitely be of use here ;-)

[Kenny Lau]

Plasmodium: Verified Horner's method

[Mohammad Pedramfar]

Donald Sebastian Leung said:

Patrick Massot said:

Math rendering at https://www.codewars.com/kata/5e997f77ea84170016600045 is painful to see. It brings back memories of the 90's.

Yeah, sorry about that, I don't think Codewars supports TeX / MathJAX or similar so I had to typeset the LaTeX in an external editor, take screenshots of the rendered output, upload them onto imgur and paste the images there.

There might be a way to get rid of that white background by using SVGs but I'm not all too familiar with it.

png images support transparent backgrounds, which could help:
https://tex.stackexchange.com/questions/287481/using-latex-to-generate-png-images-of-an-equation
but if there is dark mode and light mode in the settings, that could fail, since you either choose the text colour for the LaTeX to be black or white.

Alternatively, you might be able to convert LaTeX into HTML and then put it in the page. I haven't used pandoc before, but I've heard it's a very powerful tool. Check out example 17 in this page : https://pandoc.org/demos.html

[Patrick Massot]

Converting LaTeX to HTML using pandoc or plasTeX or other heavy programs would be overkill. They simply need to use mathjax. Maybe they don't want mathjax on all their webpages but we would need to know many more details to give advice.

[Mohammad Pedramfar]

Yes, MathJax is ideal and it canbe implemented with minimal hassle. Basically a few lines of code for the whole website, including the configurations.
What I was saying is only useful if the webpage is not changed and you can only write some html, and you can't inject javascript in the middle :grinning_face_with_smiling_eyes:

[Donald Sebastian Leung]

Patrick Massot said:

Converting LaTeX to HTML using pandoc or plasTeX or other heavy programs would be overkill. They simply need to use mathjax. Maybe they don't want mathjax on all their webpages but we would need to know many more details to give advice.

I've just checked and someone did make such a feature request back in mid-2018. Feel free to show your support by upvoting Codewars/codewars.com#1527 :grinning_face_with_smiling_eyes:

[Reid Barton]

Prof. Buzzard your Easy Fermat kata was quite difficult.

[Chris Hughes]

Was it easier than Fermat's last theorem though?

[Reid Barton]

I guess

[Donald Sebastian Leung]

@Patrick Massot I've changed N to a natural number in my definition of the sequence limit throughout the kata series if you would like to take another look at it

And thanks @Mohammad Pedramfar for your amazing idea - the descriptions look a lot nicer now :grinning:

[Patrick Massot]

It clearly looks better.

[Patrick Massot]

But I wouldn't know how to interpret those katas. What are you allowed to use from mathlib? Do you expect people redo them from scratch or crush them using the much more general versions from mathlib?

[Donald Sebastian Leung]

Patrick Massot said:

But I wouldn't know how to interpret those katas. What are you allowed to use from mathlib? Do you expect people redo them from scratch or crush them using the much more general versions from mathlib?

Either approach is fine and there is currently no way to prevent certain parts of mathlib from being used on a per-kata basis. You may learn more about our Lean environment setup on our Wiki page.

[Patrick Massot]

I think this is the reason why Kevin is writing less conventional katas

[Donald Sebastian Leung]

BTW how easy would it be for a typical undergraduate mathematician to define "transport lemmas" between the general definition of a limit in mathlib and my specialized version and solve the kata by riding on results already proven in mathlib? Would it be easier than proving it from first principles?

[Kenny Lau]

A typical undergraduate mathematician doesn't use Lean

[Kevin Buzzard]

I think this would be hard. Shing defined a custom equiv and then asked a bunch of questions which were already in mathlib for equiv but it seemed like less work to just reprove them all than to show that eg equiv.trans implied iso.trans

[Reid Barton]

The first kata I was shown was the verified Horner's rule one and the second one was tail-recursive sum. Now that I look closer the second one uses a function but even if it used a list, it would literally be "set x = 1 in Horner's rule" but I think it's still easier to reprove it than to use the proof of Horner's rule.

[Reid Barton]

Well, probably equally easy.

[Patrick Massot]

Donald, the transport lemmas already exist in mathlib. Except you created a difficulty by putting a strict inequality in a non-standard place in the definition of limit.

[Patrick Massot]

In analysis, the convention is to put strict inequality only where necessary.

[Patrick Massot]

For instance:

import topology.metric_space.basic

attribute [instance] classical.prop_decidable

def lim_to_inf (x : ℕ → ℝ) (l : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε

open filter

example : ∀ (x y : ℕ → ℝ) l,
  (∀ n, abs (x n - l) ≤ y n) →
  lim_to_inf y 0 →
  lim_to_inf x l :=
begin
  intros x y l h hy,
  unfold lim_to_inf at *,
  simp_rw [← real.dist_eq, ← metric.tendsto_at_top] at *,
  rw tendsto_iff_dist_tendsto_zero,
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hy (λ n, dist_nonneg : _) h,
end

[Reid Barton]

Shouldn't it be abs (x n - l) ≤ ε? :upside_down:

[Patrick Massot]

Good point

[Kenny Lau]

what on earth is "Suppose x n ≤ l ≤ y n and lim n → ∞ ( x n − y n ) = 0 . Prove that lim n → ∞ x n = lim n → ∞ y n = l ."?

[Donald Sebastian Leung]

Plasmodium: Odd + Even = Odd? Even * Anything = Even? Prove it!

[Donald Sebastian Leung]

Kenny Lau said:

what on earth is "Suppose x n ≤ l ≤ y n and lim n → ∞ ( x n − y n ) = 0 . Prove that lim n → ∞ x n = lim n → ∞ y n = l ."?

I'm not sure what you're getting at, would you care to elaborate?

[Kenny Lau]

https://www.codewars.com/kata/5e997f77ea84170016600045

[Mario Carneiro]

I find it funny that in Odd + Even = Odd? Prove it! they are rejecting translations of that (Haskell) kata to Coq/Lean/Agda as it is too easy. Is there a rule that katas can't be too easy?

[Yury G. Kudryashov]

We already have squeeze thm in mathlib. Is there any reason to use a different definition of the limit?

[Mario Carneiro]

@Kenny Lau You need to use words

[Kenny Lau]

the plain text version of the maths seems to be worse than the picture rendering versions

[Mario Carneiro]

My guess is kenny is pointing out the bad formatting, but I see mathjax

[Kenny Lau]

oh what

[Donald Sebastian Leung]

Mario Carneiro said:

I find it funny that in Odd + Even = Odd? Prove it! they are rejecting translations of that (Haskell) kata to Coq/Lean/Agda as it is too easy. Is there a rule that katas can't be too easy?

It's often considered a bad idea to accept translations to languages when the difference in the difficulty between translations is significant.

For example, sorting a list of numbers in ascending order would be 8 kyu in most languages but around 4 kyu in BF so the recommended approach is to keep them two separate kata instead of making a BF translation to the existing 8 kyu

[Kenny Lau]

[Yury G. Kudryashov]

@Kenny Lau Looks better in my Firefox

[Mario Carneiro]

If I use the inspector on that piece of math, I see MathML

[Mario Carneiro]

do you?

[Donald Sebastian Leung]

Kenny Lau said:

/user_uploads/3121/kYludeEVJ4yMh3eQqrAOulUh/2020-04-20-2.png

It looks much nicer on Safari on my Mac:

螢幕截圖-2020-04-20-10.28.16.png

[Mario Carneiro]

it's possible that your browser doesn't support mathml

[Kenny Lau]

I'm using Chrome btw

[Mario Carneiro]

(I'm on FF)

[Mario Carneiro]

I get plain text on chromium

[Yury G. Kudryashov]

AFAIR google removed mathml support from chrome

[Kenny Lau]

interesting

[Yury G. Kudryashov]

After they forked from webkit

[Yury G. Kudryashov]

The reasoning sounded like "it's half-working and we have mathjax"

[Donald Sebastian Leung]

Patrick Massot said:

In analysis, the convention is to put strict inequality only where necessary.

I just checked the formal definition of a limit according to Wikipedia and it does have n ≥ N. I will fix my kata again shortly.

As for |x n - l| < ε vs. |x n - l| ≤ ε, I'll keep the former since that is what Wikipedia says (and what I have been taught in my analysis course).

[Yury G. Kudryashov]

And it agrees with the standard nhds filter

[Mario Carneiro]

Rather than requiring katas to state the definition of a limit a certain way or use a mathlib API that may advantage users with more library knowledge, we should have theorems proving the equivalence of mathlib's limit to a number of basic versions of it. That way you can convert your hypothesis to mathlib form in one line

[Donald Sebastian Leung]

KaTeX support has just been enabled for kata descriptions on Codewars :tada:

[Donald Sebastian Leung]

Plasmodium: Duality in Boolean logic

[Kenny Lau]

Translated beta: But WHY is LEM unprovable?

[Andrew Ashworth]

I think you left in a bit from Coq: "A word of advice
Don't bother going through every axiom. Use Ltac instead."

[Kevin Buzzard]

You also left in an inane comment: "You can learn more about Heyting algebra and intuitionistic logic with the help of search engines.". Can you give me an X such that you cannot learn more about X with the help of search engines? Nobody needs to be told this nowadays, surely.

[Reid Barton]

X = search engines?

[Kevin Buzzard]

Nice Goedelesque try but I'm not so sure. Anyway, in the mean time you should try my generalised Pell equation $x^2-37y^2=3$.

@Patrick Massot you mentioned my choice of Kata questions. Elementary number theory is a great source of questions which are easy to state but can be very hard to prove. I am just trying to come up with kata for which you have to know some number theory techniques in order to do the maths, and then there's still a challenge of formalising it in Lean within the time limit (16 seconds sounds like a lot but I am not convinced that their test servers have got too many cores...).

[Mario Carneiro]

Reid Barton said:

X = search engines?

To be fair, you can learn more about search engines using search engines

[Simon Hudon]

If I learned anything from the IT Crowd it's that you'd don't want to type Google in Google

[Mario Carneiro]

@Kevin Buzzard To be honest I feel a bit trolled by your katas. It's probably a difference in mentality, but I almost never do formal maths problems where I don't already more or less know the answer in regular maths. For me the interesting challenge is in figuring out how to structure that understanding into something that the computer will like. In programming katas I would think it is the same way; you are given a task, and you the programmer don't have any trouble understanding the task but your job is making the computer understand it too.

With your maths puzzles, it's more like solving a Putnam problem, followed by a formalization problem. Which is fine as far as it goes, but somehow doesn't feel like "what I signed up for". My ability to come up with a good formal proof now depends on also coming up with the right mathematics, and here I don't think I can beat the many hundreds of years of effort already spent in this direction by others. Now I'm sure that most of this is your intent, I know you like maths puzzles like this, but I wonder whether it would be better to offer a solution or at least a pointer to where someone can learn the necessary tricks to solve the maths part of the problem to return the focus to the coding part (on a site like Codewars).

[Donald Sebastian Leung]

Here's an easy kata on continuous functions

[Kevin Buzzard]

Mario I completely agree with what you're saying, it is not at all clear how to do these hard number theory questions in maths. The reason I'm setting them is simply because as someone with a background in number theory and in Olympiad training as well as some Lean knowledge I am in a good position to be able to write Kata of this form. I can quite imagine that people like you will find them extremely hard for non-lean reasons but fortunately there are 40 Lean Kata out there not set by me and you can stick to them. I'm just offering something completely different because I know there are professional mathematicians out there who look at Putnam and IMO problems when they come out, and might be tempted to look at these too. You can often find the maths solutions by googling, and for the ones you can't perhaps a stackexchange question will appear or whatever. I'm intentionally offering something different, intended to appeal to different people to the usual.

[Mario Carneiro]

By the way, I didn't want to suggest that I can't do them, I have some math competition background too ;) But I would not be surprised if your kata have extremely low solve rates, because you are probably targeting the wrong audience (which is to say, a different audience than the one that frequents the Codewars site).

[Kevin Buzzard]

I was specifically aiming for low solve rates

[Kevin Buzzard]

I have already been moaning on Twitter that someone other than me solved the 5^5^5^5^5 question

[Mario Carneiro]

indeed, you might even be targeting a demographic that almost doesn't exist, namely people who are good at both maths and theorem provers

[Kevin Buzzard]

That's exactly what I'm doing

[Kevin Buzzard]

I totally agree that if I were the only person setting Lean Kata then this would be a terrible idea

[Mario Carneiro]

is this a job application in disguise? :D

[Kevin Buzzard]

But to be honest the kind of Kata that annoy me are the ones which have no maths in at all beyond elementary school but which you can't solve with dec_trivial because it takes too long. There are far far more of these

[Kevin Buzzard]

I have no interest in algorithms

[Kevin Buzzard]

I think you and I Mario understand each other's interests quite well and we also are both very clear about where we diverge.

[Mario Carneiro]

I'm not a big fan of problems that boil down to a large search. I think people gravitate to these because they think that's what computers are good for

[Mario Carneiro]

I am happy to solve those in a CAS and worry about proving correctness of the CAS later

[Kevin Buzzard]

I guess as a side comment, my kata statements would be trivial to translate into e.g. Coq, but to get them onto Codewars you'll have to offer a Coq solution so you'll have to find a Coq version of me, and encouraging a Coq version of me to exist would be something else that I'd consider a step in the right direction.

[Kevin Buzzard]

As well as aiming for low solve rates I'm aiming to make a broader class of Kata than I'm seeing in the other languages

[Kevin Buzzard]

I see that we now have 51 Lean Kata in total.

I saw someone moaning (on the codewars gitter chat maybe?) a week or two ago that it was silly to support all these obscure beta languages which had < 100 kata, and at the time it occurred to me that perhaps Lean would end up as one of those languages. But 50 is a respectable number and it would be great to get it up to 100. If anyone has any quirky little maths questions which they have solved themselves in Lean and would like to see as a kata, they should feel free to get in touch with me and I can stick it up on the site and give them attribution. I am typically solving one kata a day at the minute, in the evenings after my day job is done; yesterday I proved that $SL_2(\mathbb{N})$ was a free monoid on 2 generators in Lean (modulo an application of Euclid's algorithm which is left implicit in the question).

[Kevin Buzzard]

I just saw on Twitter that (a) Coq just moved from beta to stable in codewars, (b) Coq has been on Codewars for nearly a year and (c) they have 74 Coq kata in total.

[Kevin Buzzard]

@Jason KY. I published your kata on limits of sequences in a metric space here. It was more of a hassle than I had expected: I needed to do a letI dance in Preloaded, and an @ dance in the test case, because the question involved a typeclass.

[Jason KY.]

Thank you for publishing it! :D

[Donald Sebastian Leung]

Wow so we just had a flood of Lean kata getting approved - the total number of approved Lean kata skyrocketed from about 25 to 36 (and still increasing) :joy:

[Kevin Buzzard]

@Donald Sebastian Leung what do we need to get out of beta?

[Kenny Lau]

Donald Sebastian Leung said:

Generally, the number of satisfaction votes, rank assessments as well as the satisfaction rating required for a Beta kata to leave Beta decreases as 1) the average assessed rank of the kata is higher and 2) you get more and more kata approved. For example, if you currently have < 10 approved kata and the average assessed rank of your Beta kata is in the 7-8 kyu range then it will require 12 (satisfaction + ranking) votes with a satisfaction rating of >= 80% in order to be eligible to leave Beta, but if its average assessed rank is 1-2 kyu then it only requires 5 votes and >= 70% satisfaction to leave Beta.

You may learn more about the Beta Process on our Wiki; specifically, the kata approval requirements.

[Kenny Lau]

@Kevin Buzzard also Donald and I's votes count 4 times

[Kenny Lau]

(I still haven't figured out whether it's "Donald and I's" or "Donald's and my"

[Shing Tak Lam]

That's the beta for a Kata, not a Language?

[Kenny Lau]

oh, I misunderstood

[Kevin Buzzard]

Coq just got out of beta with 76 Kata, it took them a year

[Kevin Buzzard]

I was wondering whether the year was because it takes a year to get out of beta or because it took them a year to get 76 kata

[David Wärn]

Given a (rather long) kata solution that takes more than 16s to compile, how might I go about optimizing it? Is there a tool that would show me how much time is spent compiling each step?

[Bryan Gin-ge Chen]

set_option profiler true

[Kevin Buzzard]

My solution to $|R^\times|=5$ took more than 16 seconds to compile so I just gave up and decided to wait to see if there was a rule change :-) Kenny is the master of speeding solutions up.

[Kenny Lau]

in short: don't use simp, don't use ring, etc

[Kenny Lau]

and optimize the "proof tree"

[Kenny Lau]

you can send me the code in DM and i can optimize it when i am free and willing

[Kevin Buzzard]

It's a dismal process. I have a kata proof in another window which is taking a long time, and the only way I will be able to speed it up is to replace 10 applications of linarith with rw sub_lt_iff_lt_add or whatever; I usually cannot be bothered to do this because for me this is anti-(the whole point of linarith).

[Kenny Lau]

Kevin Buzzard said:

My solution to $|R^\times|=5$ took more than 16 seconds to compile so I just gave up and decided to wait to see if there was a rule change :-) Kenny is the master of speeding solutions up.

I'm good at it because I have to

[Donald Sebastian Leung]

Kevin Buzzard said:

I was wondering whether the year was because it takes a year to get out of beta or because it took them a year to get 76 kata

Unlike the kata approval process, there's no hard rule on when a language leaves Beta on Codewars. In fact, just not too long ago, kazk admitted that many languages were stuck in Beta for way too long since there wasn't much space left on the landing page.

Anyway, considering the rate at which Lean content is being added to Codewars (which is much faster than Coq by the way due to the active participation by the Lean community here, well done!), I think it shouldn't take a year before I can convince kazk that Lean is ready to move out of Beta - a few months (at most) should suffice.

[Kenny Lau]

beta: Index 2 subgroup is normal

[Donald Sebastian Leung]

0.999... = 1? Prove it! was supposed to be the introductory kata to my mathematical analysis kata collection, but somehow ended up being the last one to be published :stuck_out_tongue:

Anyway, I think I've authored enough Lean kata for now

[Donald Sebastian Leung]

/me switches from kata authoring mode to kata solving mode

[Sebastien Gouezel]

Kenny Lau said:

beta: Index 2 subgroup is normal

Could we have this in mathlib? :)

[Johan Commelin]

Nope... that would be a spoiler.

[Donald Sebastian Leung]

PSA: The time limit for Lean on Codewars has been extended to 20s

[Kevin Buzzard]

Time to try my collection of solutions which time out :-)

[Kenny Lau]

beta: Group Is Not Union Of Two Proper Subgroups

[Donald Sebastian Leung]

Kevin Buzzard said:

Donald Sebastian Leung what do we need to get out of beta?

@Kevin Buzzard I've just got a definitive reply from kazk: (s)he is willing to consider moving Lean out of Beta early if we manage to get 50 approved kata (currently 38).

[Kenny Lau]

I still feel it's too early. But if you (and the Lean community) believe it's ready, maybe after 50 approved kata.

[Kenny Lau]

that sounds anything but definitive.

[Kenny Lau]

also what about all other languages with 50 approved kata

[Andrew Ashworth]

What does beta status mean on Codewars? What's going to happen when Lean 4 comes out to these kata?

[Steffan]

@Andrew Ashworth It's basically a state of a language where it may still have bugs and is not yet a primary language on CW.

[Steffan]

beta: Index 2 subgroup is normal

beta: n(n+1)(4n-1)/6

[Steffan]

Now not beta, thanks to Voile :)

[Kenny Lau]

wow that's the fastest any kata has gone from beta

[Steffan]

I published it last night tho

[Steffan]

still, that was fast

[Steffan]

now there's 40 approved lean kata

[Steffan]

uh oh, you reacted in the wrong order, it's 0 4 instead of 40. ;)

[Steffan]

10 more to go

[Kevin Buzzard]

I should make some easier ones. I'll have a go this weekend

[Steffan]

but you haven't solved mine yet :o

[Kevin Buzzard]

I wanted to make some stupidly hard ones but if the aim is to get to 50 then perhaps now is the time for some mathematically simpler ones. Which one is yours? The 4n-1 one? I am cautiously optimistic I can do it

[Steffan]

Yes, the 4n-1 ones is mine

[Sebastien Gouezel]

Are very hard katas allowed, like

def collatz (n : ℕ) : ℕ := if (n % 2) = 0 then n/2 else (3 * n + 1)

theorem not_so_easy (n : ℕ) : ∃ k, collatz^[k] n ≤ 1 := sorry

[Kenny Lau]

how is my subgroup union not out of beta

[Kenny Lau]

@Sebastien Gouezel you need to be able to solve it yourself

[Steffan]

It doesn't have enough solves, so it's not approvable

[Sebastien Gouezel]

I can solve it, but it doesn't fit in this tiny 16s margin.

[Steffan]

20s

[Sebastien Gouezel]

Even 20s would not be enough for my solution :)

[Kevin Buzzard]

I can resolve it in aleph_null seconds, maybe we should ask for a time extension

[Kevin Buzzard]

def collatz' (n : ℕ) : ℕ := if (n % 2) = 1 then n/2 else (3 * n + 1) Maybe this one is easier?

[Steffan]

It already was extended to 20s

[Kevin Buzzard]

unfortunately I'm not sure they'll let us go as far as aleph_null

[Steffan]

what's that?

[Steffan]

is it infinite time I guess? ℵ0

[Mario Carneiro]

https://en.wikipedia.org/wiki/Aleph_number#Aleph-naught

[Mario Carneiro]

"infinity" is such an imprecise term

[Reid Barton]

You should really be using ordinals for the runtime of your transfinite computations.

[Jalex Stark]

is it possible to make "prove example {p : Prop} : ¬¬¬p → ¬p without classical reasoning" a kata? maybe by disallowing certain imports?

[Johan Commelin]

If codewars can do #print axioms SOLUTION and inspect the result...

[Jalex Stark]

Johan Commelin said:

If codewars can do #print axioms SOLUTION and inspect the result...

okay, I think the answer to that is yes, and if so @Donald Sebastian Leung would know how to do it

[Kenny Lau]

or... we can build a proposition logic system

[Donald Sebastian Leung]

Jalex Stark said:

is it possible to make "prove example {p : Prop} : ¬¬¬p → ¬p without classical reasoning" a kata? maybe by disallowing certain imports?

We deliberately made the Lean setup very simple and allow the usual mathematical axioms without restriction since we were told that mathematicians do not even consider the use of non-constructive axioms something worth mentioning about. If you want to author a Lean kata where these axioms matter then someone will have to implement a proper testing framework for Lean like what monadius did for Coq. This (adding a dedicated testing framework now) would also mean that the Beta phase for Lean itself on CW will most definitely have to be extended in order to allow sufficient time for us to detect and fix any errors in the testing framework so just having 50 approved kata will no longer cut it.

[Donald Sebastian Leung]

An alternative would simply be to author this kata in Coq instead, where we do already have a proper testing framework for specifying allowed axioms on a per-kata basis. But, no offense, I doubt the Coq community on CW would welcome such an exercise given that it can be solved using a simple tauto.

[Mario Carneiro]

Aren't you already testing that proofs don't include bad axioms?

[Donald Sebastian Leung]

Yes, but for our current Lean setup, the set of allowed axioms is hardcoded so it cannot be customized on a per-kata basis.

[Steffan]

You can't have infinite time, because if you did, then if you had an infinite loop, it would never stop running. It is inside a Docker image so it shouldn't be too hard to terminate, but it makes extra work. Who knows, you might crash Docker or something.

[Patrick Massot]

Steffan, there really mean infinite here. Arbitrarily long is not enough.

[Steffan]

No, I mean that on CW, it wouldn't really work to have infinite time for the reason I explained.

[Kevin Buzzard]

I think that my proposed proof of Collatz ("check all cases") has several other issues as well as the limitations of CW.

[Jalex Stark]

Steffan said:

No, I mean that on CW, it wouldn't really work to have infinite time for the reason I explained.

Yes, I think everyone in this discussion understood that codewars can't support infinite time solutions, and this was proposed as a joke.

[Jalex Stark]

Donald Sebastian Leung said:

An alternative would simply be to author this kata in Coq instead, where we do already have a proper testing framework for specifying allowed axioms on a per-kata basis. But, no offense, I doubt the Coq community on CW would welcome such an exercise given that it can be solved using a simple tauto.

Sad! I will give up on making this a kata. I will still tell students to do this exercise. I think it's a good example of how "follow your nose with the tactics you know" can result in Lean teaching you something new.

[Jalex Stark]

Kenny Lau said:

or... we can build a proposition logic system

Hmm. So the solution I have in mind for a beginner who follows their nose is like this

example (p : Prop) : ¬ ¬ ¬ p → ¬ p := begin
-- your goal is an implication, so intro stuff
intros h hp,
-- you've only got one lemma, so apply it
apply h,
-- again, your goal is an implication, so intro stuff
intro hnp,
-- now we've got a contradiction in our hypotheses!
exact hnp hp,
end

[Jalex Stark]

I'm having a hard time imagining making my own propositional logic such that the proof can be found through essentially the same "follow your nose" algorithm

[Mario Carneiro]

Why can't it be a kata anyway? Just make it a low difficulty kata

[Jalex Stark]

Mario Carneiro said:

Why can't it be a kata anyway? Just make it a low difficulty kata

I guess as a beginner you could have the experience of submitting a classical proof and then being surprised that others did it without by_cases or not_not or whatever you used. (and I guess also learning that tauto exists)

[Mario Carneiro]

Just say in the rules for the kata that it should be intuitionistic, and optionally say that you won't be marked off for using a classical proof

[Jalex Stark]

Is this table accurate? It says that one needs 300 honor to propose kata https://airtable.com/embed/shrDt7USqZ7GStRb0/tblk0mEQbDl3JWQrT/viwdZcVcThJKTXyuB?blocks=hide

[Steffan]

Yes, that's correctr.

[Steffan]

I recommend the CW wiki tho: https://github.com/codewars/codewars.com/wiki/Privileges

[Jalex Stark]

Steffan said:

I recommend the CW wiki tho: https://github.com/codewars/codewars.com/wiki/Privileges

Thanks! It's anybody's guess why : 1. the thing I linked is public 2. google brought me there instead of here

[Kevin Buzzard]

I blitzed a bunch of Lean kata to get to 300 -- Kenny blitzed a bunch of python kata. It didn't take long. Don't bother with 8 kyu stuff, the smaller kyu problems give you far more honor

[Jalex Stark]

yeah I think I will do the python route. The harder kata are hard for me :P

[Sebastien Gouezel]

Kevin Buzzard said:

Nice Goedelesque try but I'm not so sure. Anyway, in the mean time you should try my generalised Pell equation $x^2-37y^2=3$.

Do you expect the traditional way of solving Pell equations (I mean, bringing it back to a bounded domain by multiplication by a fundamental unit, and then case bashing there), or is there a trick for this one?

[Kevin Buzzard]

I did it the way you are suggesting. I know of no other way. 3 splits into two non-principal primes.

[Matt Earnshaw]

for the 0.999... = 1 kata I am stuck on this confusing error (omitting some potential spoiler state). I tried turning off pp.notation to check the terms but they really are syntactically equal

33:3: rewrite tactic failed, did not find instance of the pattern in the target expression
  abs (9 / 10 * geom_series (1 / 10) n - 1)
state:
ε : ℝ,
n : ℕ,
⊢ abs (9 / 10 * geom_series (1 / 10) n - 1) < ε

[Jalex Stark]

Matt Earnshaw said:

for the 0.999... = 1 kata I am stuck on this confusing error (omitting some potential spoiler state). I tried turning off pp.notation to check the terms but they really are syntactically equal

33:3: rewrite tactic failed, did not find instance of the pattern in the target expression
  abs (9 / 10 * geom_series (1 / 10) n - 1)
state:
ε : ℝ,
n : ℕ,
⊢ abs (9 / 10 * geom_series (1 / 10) n - 1) < ε

probably some of those literals are getting interpreted in the integers when you wanted them in the reals or similar. If you post a #mwe then maybe someone can help you.

[Matt Earnshaw]

@Jalex Stark aha, now I see set_option pp.numerals false which indeed reveals a mismatch of the form you suggest. I should be able to fix it now, thanks

[Jalex Stark]

Ooh nice! I'll try that next time I get an error like this

[Steffan]

@Kevin Buzzard For a kata, what about something like a ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)? I couldn't prove it lol

[Johan Commelin]

by ring

[Steffan]

nope

[Johan Commelin]

Stupid ring

[Steffan]

doesn't do it

[Johan Commelin]

Where do a and b live?

[Alex J. Best]

ring_exp?

[Johan Commelin]

If a and b are natural numbers, then this is :head_bandage:

[Steffan]

@Johan Commelin Not sure what you mean
@Alex J. Best doesn't work :/

[Steffan]

a and b are nats

[Johan Commelin]

Aha...

[Steffan]

ring changes the goal to a ^ 4 - b ^ 4 = (((a + b) * a + b ^ 2) * a + b ^ 3) * (a - b)

[Kevin Buzzard]

If you're foolish enough to use nat subtraction then don't blame me ;-) Is it even true for nats?

[Steffan]

I'm quite sure it's true

[Steffan]

I found it online

[Johan Commelin]

If a < b then both sides are 0

[Kevin Buzzard]

Yeah it's true, and I guess I wouldn't find it hard to prove, but I know lots of tricks with these things now

[Steffan]

WolframAlpha says it's true too

[Kevin Buzzard]

rofl

[Johan Commelin]

No it doesn't

[Kevin Buzzard]

ask WA if it says a-b+b=a for nats

[Kevin Buzzard]

and if it does then file a bug report because 0-1+1 isn't 0 as any fule kno

[Johan Commelin]

How does WolframAlpha know about nat.sub

[Steffan]

more like, how does it know n >= 0

[Steffan]

@Johan Commelin what do you mean it says false

[Kevin Buzzard]

WA surely does not know about Lean's stupid nat.sub function

[Kevin Buzzard]

If you type - into WA then it does not interpret it as nat.sub but your question is about nat.sub

[Johan Commelin]

@Steffan How do you tell WA to use natural numbers instead of integers or reals?

[Kevin Buzzard]

If you say a>=0 and b>=0 then it will still not use nat.sub

[Steffan]

It needs to know that the result must be >= 0, and you cant do that afaik

[Kevin Buzzard]

exactly

[Kevin Buzzard]

and that's why we are saying that WA can't check the result. It's certainly true for any commutative ring, but nat isn't a ring

[Steffan]

so I need to prove a ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2) with ints?

[Steffan]

yep, ring does it

[Steffan]

too easy

[Kevin Buzzard]

Exactly

[Kevin Buzzard]

Of course ring does it, it's true in all commutative rings

[Johan Commelin]

@Steffan Ask Lean #eval 1 - 2

[Kevin Buzzard]

The difficulty with your question is that the - is nat.sub which is a pathological function

[Johan Commelin]

And see whether WA agrees with Lean :stuck_out_tongue_wink:

[Johan Commelin]

Yup, it's a trap...

[Steffan]

I know that 1 - 2 = 0 for nats.

That sure was a trap.

[Kevin Buzzard]

That's why the question is hard. ring works under assumptions like a-b+b=a which are not true for nats

[Johan Commelin]

So... you can actually make it a kata, if you want. But it would be pathological.

[Johan Commelin]

Hint, first prove a^2 - b^2 = (a - b) * (a + b) as a helper lemma.

[Johan Commelin]

After that, it shouldn't be too hard.

[Steffan]

so it is actually true with nats? I didn't bother to bother my brain

[Kevin Buzzard]

Yes!

[Kevin Buzzard]

Because by luck, both sides are zero if b>a

[Steffan]

ok, I'll try, thanks

[Kevin Buzzard]

example (a b : ℕ) : a^2 - b^2 = (a-b)*(a+b) :=
begin
  by_cases h : b ≤ a,
  { rw le_iff_exists_add at h,
    cases h with c hc,
    rw hc,
    -- multiply out and sort things out
    sorry
  },
  { -- show both sides are 0
      sorry
  }
end

[Steffan]

thanks, but I don't think I'm good enough at lean to do that, that's why I tagged you about the proof

[Kevin Buzzard]

import tactic

example (a b : ℕ) : a^2 - b^2 = (a-b)*(a+b) :=
begin
  by_cases h : b ≤ a,
  { rw le_iff_exists_add at h,
    cases h with c hc,
    rw hc,
    rw (show (b+c)^2 = c^2+2*b*c+b^2, by ring),
    rw nat.add_sub_cancel,
    rw add_comm b c,
    rw nat.add_sub_cancel,
    ring,
  },
  { -- show both sides are 0
    push_neg at h,
    replace h := le_of_lt h,
    have h2 : a^2 ≤ b^2,
      apply nat.pow_le_pow_of_le_left h,
    rw ←nat.sub_eq_zero_iff_le at h h2,
    rw [h, h2, zero_mul],
  }
end

[Kevin Buzzard]

now see if you can do a^4-b^4 from there :-)

[Johan Commelin]

lemma foo (a b : ℕ) : a ^ 2 - b ^ 2 = (a - b) * (a + b) :=
begin
  by_cases h : b ≤ a,
  { obtain ⟨c, rfl⟩ : ∃ c, a = b + c, by rwa le_iff_exists_add at h,
    simp [nat.pow_two, add_mul, mul_add, nat.mul_sub_right_distrib, mul_comm b c, add_comm] },
  { push_neg at h,
    rw [nat.sub_eq_zero_of_le (le_of_lt h), zero_mul],
    apply nat.sub_eq_zero_of_le (le_of_lt _),
    rwa nat.pow_lt_iff_lt_left (show 1 ≤ 2, from dec_trivial) }
end

example (a b : ℕ) : a ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2) :=
begin
  rw [← foo, ← foo],
  simp [nat.pow_succ, mul_assoc],
end

[Steffan]

wow, but I don't want to steal all that code, you guys can make a kata!

[Johan Commelin]

Go ahead... I'm not (yet) on CW.

[Johan Commelin]

This code is in the public domain.

[Reid Barton]

now you can't because of spoilers

[Kevin Buzzard]

I don't have any particular desire to show off how hard it is to work with a pathological function such as nat.sub

[Steffan]

I can do it if you guys delete your messages, then the spoiler will be gone. I've copied everything into my "scratchpad"

@Johan Commelin your foo is so awesome that I cannot understand it :D

[Johan Commelin]

foo says that either stuff works as you expect, or both sides are zero. If things work as you expect, you make life easier by replacing b with a + c, for some natural number c. After that, you just follow your nose. If things are zero, then you show this by searching the library for the fact that a < b implies a^2 < b^2.

[Steffan]

Anyway, would you mind editing out the code you posted so I can publish the kata?

[Kevin Buzzard]

Editing out the code does not remove it, you can always look at the edit history.

[Steffan]

So do you suggest I just publish it?

[Steffan]

Or if you delete the comment, that might work

[Kevin Buzzard]

Johan posted the proof, I just posted a hint. Why don't do you a^6-b^6 instead if you're worried?

[Mario Carneiro]

Here's a strategy that works for most ring-like problems on nat.sub:

import tactic.ring

example (a b : ℕ) : a ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2) :=
begin
  cases le_total a b with h h,
  { rw [nat.sub_eq_zero_iff_le.2 h, zero_mul, zero_mul,
        nat.sub_eq_zero_iff_le.2 (nat.pow_le_pow_of_le_left h _)] },
  { apply int.coe_nat_inj,
    simp [int.coe_nat_sub, h, nat.pow_le_pow_of_le_left h _],
    ring },
end

[Scott Morrison]

I really don't think we should censor code or conversations on Zulip for the sake of CW.

[Jalex Stark]

I think math.stackexchange is a good reference point, they have a lot of posts which are good content but also can be used to cheat on undergrad homework

[Donald Sebastian Leung]

Scott Morrison said:

I really don't think we should censor code or conversations on Zulip for the sake of CW.

I realize I may have gone a bit overboard initially with this "no spoilers" thing, sorry about that :sweat_smile: To clarify, we do try to minimize spoilers whenever possible but it's not meant as a hard rule, so, e.g. hints and general directions are often acceptable. As for full solutions, IMO posting them here on Zulip is also fine since messages come and go and a cheater would have to deliberately scour through the chat to find these spoilers, but just don't, e.g. create a public GitHub repository specifically containing solutions to Codewars kata and draw attention to it by, e.g. naming it "Codewars-Solutions" and/or asking others to actively contribute to the repo.

The general policy for spoilers and cheating on Codewars is: making solutions publicly available is technically allowed but discouraged; plagiarizing solutions to gain free points is disallowed and could get you banned.

[Jalex Stark]

I finally have enough honor to post kata! I'm confused about what I'm supposed to put in the "preloaded" and "test" sections. Can anyone advise?

[Shing Tak Lam]

Preloaded is where you put code where you don't want the user to modify, so definitions, structures etc.

Test is where you make sure the people solving the kata didn't use sorry. Take a look at an existing Kata.

[Jalex Stark]

hmm... Is there a way to extract the testing code from a kata page? I imagine not, since in most languages that would let you solve it by hardcoding the tests

[Jalex Stark]

(and in particular, i visited a few kata to try to extract this information and couldn't find it)

[Shing Tak Lam]

That's why there are Example Tests, which are visible to the user, and the actual tests, which are not.

[Jalex Stark]

are there Lean kata with visible example tests? the random first two i tried didn't have them

[Shing Tak Lam]

Mhm... I think for a lot of Lean kata, the actual tests and the example tests are the same.

[Jalex Stark]

okay, I'll try harder and then come back when I have a more interesting failure mode

[Shing Tak Lam]

image.png

The bottom right corner is the example tests.

[Shing Tak Lam]

and you can see on the left that most Lean kata have the preloaded file copied into the description, as there is no way to access Preloaded.lean when solving the kata.

[Jalex Stark]

Okay, I think I managed to post a working kata (it is very much 8 kyu)
https://www.codewars.com/kata/5eb0ce255179590016d613ce/train/lean

[Steffan]

Scott Morrison said:

I really don't think we should censor code or conversations on Zulip for the sake of CW.

Okay, so I decided to publish this: https://www.codewars.com/kata/5eac8d8845655d003300f5b5

[Donald Sebastian Leung]

We now have 45 approved Lean kata, way to go! We only need 5 more before bugging kazk again to get Lean support out of Beta once and for all :wink:

[Kenny Lau]

beta: New induction scheme on integers

[Markus Himmel]

Two fresh beta kata: Linear projection and Squareful segments

[Kenny Lau]

@Markus Himmel my solution is shorter than your solution for the second one

[Markus Himmel]

Kenny Lau said:

Markus Himmel my solution is shorter than your solution for the second one

Argh, I refactored the problem until the statement made no sense any more.

[Markus Himmel]

Kenny Lau said:

Markus Himmel my solution is shorter than your solution for the second one

Alright, I hope it's fixed now.

[Kenny Lau]

oh no my solution became invalid

[Kevin Buzzard]

That'll teach you :-)

[Jalex Stark]

Has anyone thought about writing kata that expect you to write a tactic? It could work like kata in non-theorem language, where there's a suite of test lemmas that your tactic has to solve, and the kata might not show you all of the tests.

[Aniruddh Agarwal]

Can I view my current goals when using tactics on codewars?

[Jalex Stark]

No, you should program everything locally and then submit it once it compiles on your machine

[Donald Sebastian Leung]

Jalex Stark said:

Has anyone thought about writing kata that expect you to write a tactic? It could work like kata in non-theorem language, where there's a suite of test lemmas that your tactic has to solve, and the kata might not show you all of the tests.

@Jalex Stark That would most definitely be possible. In Coq we have Rewriting on any binary equivalence relation which requires the solver to tap into a Coq-specific language feature in order to make the rewrite tactic work on modular equality as opposed to the usual equality. We also have Ltac practice: The tarai function which doesn't require you to write your own automation, but is much easier if you do so (which is the point of the kata).

The good thing about both of these kata is that their tests do not rely on any fancy features from the testing framework so they should be doable in Lean as well.

[Donald Sebastian Leung]

Aniruddh Agarwal said:

Can I view my current goals when using tactics on codewars?

To add to what Jalex said, you may learn more about the Lean setup on Codewars on our Wiki.

[Kevin Buzzard]

@Jalex Stark that's a really interesting idea! There's a way of just being able to make a tactic by chaining other tactics so one could think about doing that, and of course you'll have to avoid tactics which are already there eg the canonical exercise "write an assumption tactic" probably can't be done because you can just use assumption, but there's an example in Programming in Lean of some sort of first order logic tactic which might work.

How will you check the user only used their tactic though? Can this be made part of the framework?

[Donald Sebastian Leung]

How will you check the user only used their tactic though? Can this be made part of the framework?

I think Jalex's idea is that the solver will not be proving theorems at all, only implementing the required tactics, and then the test cases themselves will contain theorem statements and proofs using the tactic(s) defined by the solver, which, if implemented correctly, should compile with no errors (and not insert sorrys / forbidden axioms). So in that case, the solver will have no (direct) control over which tactics are being used in the proofs.

But if you mean whether one can ensure that the solver-defined tactic does not invoke a particular built-in tactic, then no, this is not possible with the current setup.

[Jalex Stark]

Yeah I agree with Donald. To be a tiny bit more explicit, the initial solution would look like

meta def submission_tactic :=

and the test cases would look like

example : test_prop1 := by submission_tactic
example : test_prop2 := by submission_tactic

[Jalex Stark]

So an 8 kyu "tactic-writing hello world" might have an answer that's morally equivalent to

meta def submission_tactic := repeat {apply lemma1 <|> apply lemma2}

and the test cases are things that fall to (possibly long) repeated applications of lemma1 and lemma2. That probably means that

meta def submission_tactic := simp only [lemma1, lemma2]

works too, but I'd be fine with that.

[Kevin Buzzard]

I see! That sounds like a great idea! I have no interest in tactic-writing myself but I certainly know mathematicians who are interested

[Bhavik Mehta]

I agree with Donald and Jalex that this is a good idea

[Jalex Stark]

well if i manage to teach myself enough about writing tactics, I'll go on to create some kata about it
(but mostly I am learning automation at exactly the rate that it makes the math I want to do easier)

[Bhavik Mehta]

Kevin Buzzard said:

unfortunately I'm not sure they'll let us go as far as aleph_null

I managed to get this to work! It's only for even integers, but still! A Kata for the Goldbach conjecture Part 1, Part 2, contains a spoiler for Part 1.

[Kenny Lau]

@Bhavik Mehta I have left a comment on Part 1

[Bhavik Mehta]

Thanks for that, amended

[Bhavik Mehta]

Of course your solution to part 2 is cleaner than mine!

[Kenny Lau]

@Bhavik Mehta aha, I have a cleaner solution yet

[Kenny Lau]

@Bhavik Mehta posted

[Bhavik Mehta]

Haha I just thought of that after you said you had a better one!

[Kenny Lau]

also all the 2*n should be n

[Bhavik Mehta]

oops. You can tell what the earlier versions were like

[Mario Carneiro]

Um, I've disproved Part 2

[Mario Carneiro]

so if you've managed to prove it then lean is inconsistent

[Bhavik Mehta]

:) :)

[Mario Carneiro]

oh I see, you are teaching bad habits

[Bhavik Mehta]

Let's frame it as: what happens when we follow bad habits

[Bhavik Mehta]

I was inspired by katas like this where a solution involves doing the sort of thing which you shouldn't really be doing

[Chris Hughes]

Kenny Lau said:

also all the 2*n should be n

I thought this was the deliberate mistake and I was googling for a proof in the case n is a multiple of 4.

[Reid Barton]

Why not just work one out for yourself? :upside_down:

[Kenny Lau]

1. We now have 46 approved kata!
2. Should we have a CW stream?

[Patrick Massot]

I'd be in favor of a CW stream. I'm very happy to have many different ways to happily use Lean, but I have zero interest in discussion involving katas and CW beta whatever

[Jalex Stark]

https://leanprover.zulipchat.com/#narrow/stream/238266-Codewars/topic/stream.20events/near/197087959