Add Lean3

[DonaldKellett]

Lean is a theorem prover based on the Calculus of Constructions. It is similar in nature to Coq. The current official stable release from Microsoft is 3.4.2, but it has been recommended to support v3.5.c instead which is a community-supported version.

N.B. Lean is currently in active development and Lean4 is expected to be out in about a year or so, though there is no official statement on the exact release date of Lean4. Since Lean4 is expected to break backward compatibility with Lean3, it has been suggested that Lean3 and Lean4 should be treated as two separate languages. This issue ticket deals with adding Lean3 support; please open a new issue ticket if you would like to request Lean4 support.

Installation

https://github.com/leanprover-community/lean/releases/tag/v3.5.1

N.B. mathlib for Lean (similar to mathcomp in Coq?) is also practically required in order to prove trivial identities such as 100 * 100 = 10000 within a reasonable amount of effort (thanks @monadius for bringing this to my attention!).

Compiling Proof Scripts

For standalone files

Suppose your proof script is Solution.lean. Then just execute the following:

$ lean Solution.lean

For multiple files (Preloaded, Solution, SolutionTest)

Initial Setup

$ leanpkg new kata
$ cd kata
$ leanpkg add leanprover-community/mathlib # Practically required; see above
$ leanpkg configure # Maybe we don't need this as this might already be done by the command above
$ update-mathlib # Download olean files from cloud to save mathlib compilation time (~30 mins!)
$ cd src

Then add .lean files (in the src/ subdirectory) as required, e.g. Preloaded.lean, Solution.lean, SolutionTest.lean

Compiling the Kata

Suppose we have two files: Solution.lean and SolutionTest.lean.

-- Solution.lean

lemma my_add_comm (m n : ℕ) : m + n = n + m :=
by simp

-- SolutionTest.lean

import Solution

#print axioms my_add_comm

Then just run lean SolutionTest.lean.

Testing Frameworks

None that I know of. But Lean has #print axioms (like Print Assumptions in Coq) so we could perhaps preprocess the output generated until we have a proper test framework available. The output of #print axioms in Lean also looks much cleaner and more regular than in Coq. E.g.

lemma trivial (n m : ℕ) : n + m = n + m :=
begin
  refl,
end

#print axioms trivial

outputs no axioms and

lemma my_add_comm (n m : ℕ) : n + m = m + n :=
begin
  simp,
end

#print axioms my_add_comm

outputs propext. Using sorry as in the following (similar to admit/Admitted in Coq):

lemma my_add_comm (n m : ℕ) : n + m = m + n :=
begin
  sorry,
end

#print axioms my_add_comm

outputs:

[sorry]
no axioms

Progress

• Install Lean v3.5.1
  • Add leanprover/mathlib
• Figure out how to support testing
• Implement test support
• Icon
• CodeMirror mode (use Agda mode for now)

---

👍 reaction might help.

[DonaldKellett]

I just recently learned from an email in coq-club revolving around the discussion on whether Coq or Lean is better that there are 3 indispensable core axioms commonly assumed in Lean, namely:

• Propositional Extensionality: propext
• Quotient Soundness: quot.sound
• Choice: classical.choice

More about these 3 axioms in Lean can be found on https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

Until we have a proper test framework for Lean on Codewars like we do for Coq (coq_codewars), here is what I think we can implement for the post-processor for testing (much simpler than for Coq):

1. Split the test output into lines
2. If there exists any line which is neither of no axioms, propext, quot.sound or classical.choice then mark that line as failed

Also, I personally think that it would be invaluable if we could eventually invite the "big players" in Lean such as Prof. Kevin Buzzard (@kbuzzard) of Imperial College London to Codewars when the time comes. This could potentially open up Codewars to a whole new audience (pure mathematicians) thereby fostering diversity, as well as potentially expanding the range of topics covered by theorem-proving Kata on Codewars to include problems in pure math as well (the current theorem-proving Kata on Codewars are largely geared towards computer science).

What do you think @kazk ?

[kazk]

I don't know anything about Lean at the moment, but it's been in my list of languages to look into since 2017-11-25 (forgot why 🤔). I'll be happy to add support for it, but will need help from you and others like how we did Coq/Agda.
We can start discussing. Is there any other Codewars user interested?

(I think the next language will be Prolog (#159) since I just found a possible way to use the standard plunit, but that shouldn't take too long.)

[kbuzzard]

I can't tell you anything about how to get it working (but for sure there will be people on the Lean chat who would be able to help) but I'd certainly advertise it if Lean were to become an accepted language...

[DonaldKellett]

Now that Coq support on Codewars is stable and ready to leave Beta at any moment, I'll probably start looking into this very soon.

[monadius]

@DonaldKellett I recommend reading this discussion about Lean support in Proving for Fun. As I understand, the main problem with Lean is that all notations are global. So it is possible to cheat by creating custom notations. I don't know if this issue was completely solved in Proving for Fun. You can see its backend code here.

[DonaldKellett]

@monadius Thanks, I will take a look at the links you posted in my spare time 👍

As I see it, the ideal case would be to add Lean support in such a way that a properly authored Lean Kata would be virtually unhackable like in Coq. But if we cannot patch all potential loopholes, I think it is okay to treat certain cheats (such as redefining notations to somehow circumvent the testing framework) like we do runner cheats in more conventional programming languages, given that it is highly unlikely for a well-meaning Codewarrior to accidentally stumble upon them.

[alexjbest]

As I recall the proving for fun approach worked quite well in the end https://github.com/maxhaslbeck/proving-contest-backends/blob/master/Lean/grader.py , with no known loopholes left. @kappelmann can probably say more but the idea is to have lean export the output file in an internal format and then check that with leanchecker.

[DonaldKellett]

@kazk I have started a discussion about this on the Lean Zulip chat, posting the link here for future reference. As suggested by one of the replies in the thread, the most suitable version of Lean for Codewars over the next 2 years or so would probably be Lean v3.5.c.

[kappelmann]

As far as I know, there is no known bug for the Lean grader for the proving for fun system. You might get an idea of how to set up a Lean grading environment from the files there.

I do not know the format that Codewars uses, but for proving for fun, we have

1. a definitions file: containing the needed definitions for the problem statement
2. a submissions file: imports the definitions file and the code written by the user
3. a check file: imports the definitions and submission file and checks whether the submission solves the problem at hand.

One problem in Lean is that it provides a strong meta framework and so a user could theoretically override the meaning of the goal statement written in the check file. To avoid this, we predefine notations for the goal statement in the definitions file. A typical problem statement hence would look something like this:

1. definitions.lean

def GOAL := ...
notation `GOAL` := GOAL -- prevents the user from overriding the goal in the check file

2. submission.lean

import .definitions

lemma user_lemma := ... -- the lemma proved by the user

3. check.lean

import .definitions
import .submission

theorem the_goal : GOAL := user_lemma

Let me know if you have any further questions (I am also on the Lean Zulip chat).

[DonaldKellett]

@kappelmann Many thanks for your link to the Proving for Fun backend and examples; I am sure that it will come in handy as a reference when we implement Lean 3 support on Codewars.

If you don't mind, I would like to ask you a few questions:

• For professional mathematicians using Lean, is there any situation where, for example, it would be useful to disallow one or more of the core axioms (propext, quot.sound, classical.choice), or, on the other hand, allow extra axioms on top of those three? If so, how often? As a reference, the Coq environment on Codewars allows the Submit Tests (the grader / check file, if you will) to specify on a Kata-to-Kata basis which axioms are allowed, in order to enable Kata authors to, e.g. enable functional extensionality where it makes sense or enable real number axioms for Kata dealing with real numbers
• In case we decide to follow the setup for Proving for Fun closely, what license is the repo you linked to under and what level of attribution would you prefer?

[kappelmann]

For professional mathematicians using Lean, is there any situation where, for example, it would be useful to disallow one or more of the core axioms (propext, quot.sound, classical.choice), or, on the other hand, allow extra axioms on top of those three? If so, how often? As a reference, the Coq environment on Codewars allows the Submit Tests (the grader / check file, if you will) to specify on a Kata-to-Kata basis which axioms are allowed, in order to enable Kata authors to, e.g. enable functional extensionality where it makes sense or enable real number axioms for Kata dealing with real numbers

I am not a mathematician, so I will link @kbuzzard once more so he can correct me or put in more thoughts about this. My tldr; is: just get started allowing only propext, quot.sound, and classical.choice and add other features (e.g. allowing more or fewer axioms) as needed.

The current maths community in Lean does use any of these axioms whenever they like. Constructivism does not play a major role in the development of the current mathematical library, so, for example, classical.choice might be invoked anytime.

However, constructivism is important if one is concerned with computation, which I assume you at Codewars are. So potentially, you might be interested in restricting certain axioms for certain problems. In Lean 3, noncomputable functions are actually marked using a noncomputable flag (see https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html). I assume one can query for these flags programmatically when checking submissions. I never had to do that, so I'd advise you to ask on Zulip if you are running into this problem in the future.

On the other hand, I think it might be interesting to allow more axioms for certain challenges. Sometimes, certain functionalities/concepts simply do not exist in the Lean library yet, but one still wants to pose a challenge involving these concepts without having to fully formalise them first. In that case, further axiomatisation would be of interest. But again: I would not bother adding this feature until it is actually needed.

In case we decide to follow the setup for Proving for Fun closely, what license is the repo you linked to under and what level of attribution would you prefer?

This might best be answered by @maxhaslbeck

[DonaldKellett]

Thanks again for your input. The primary objective of adding Lean to Codewars, at least from my perspective, is to attract a new audience to the site, namely mathematicians, and hopefully have them contribute new types of theorem-proving challenges to the platform focusing on pure mathematics as opposed to PL theory or other CS-related topics (we already have Coq/Agda for that); therefore, I think it would be beneficial to tailor the Lean environment on Codewars towards them. As it seems that mathematicians generally use those three core axioms without reservation, I think it would be fine to just enable them all of the time, regardless of whether we develop extensions to the grader to allow extra axioms to be admitted on a per-Kata basis later on.

---

@kazk I'm inclined to just go with @kappelmann 's suggestion and support the three core axioms (and only those three) for testing, perhaps by way of post-processing output generated by #print axioms. If it later turns out that not allowing for the extra flexibility of allowing/rejecting certain axioms on a per-Kata basis is a major hindrance then perhaps I can figure out how to add a dedicated testing framework later on. What do you think?

In any case, I will prepare an example setup soon and post the link here once I am done to demonstrate how Lean support could be added to Codewars.

[kazk]

@DonaldKellett Yeah, let's try post processing first and see how that goes.

[DonaldKellett]

An example setup is now available at https://github.com/DonaldKellett/cw-lean-setup-example

[DonaldKellett]

Also, I should probably add that we need to support keybindings for Lean like in Agda. Even though Unicode characters such as Ɐ do have ASCII equivalents such as forall, many mathematicians strongly prefer the Unicode counterparts over plain ASCII.

[kappelmann]

Note that #print axioms can be hijacked using metaprogramming in Lean. See this issue opened yesterday at the proving for fun system. It's safer to use a proof checker to list all used axioms. However, leanchecker (the checker shipped with lean) does not print French quotes at the moment, allowing for another cheat (also described in linked issue). You can either wait until the issue is fixed in leanchecker or use a different external Lean proof checker. I personally opt for the former as it's already shipped with Lean.

[DonaldKellett]

@kazk I have updated the examples at https://github.com/DonaldKellett/cw-lean-setup-example

For the issue about leanchecker, I think we can update our Lean version once that is fixed, but in the meantime, we can still add Lean support to Codewars, and treat the cheat demonstrated in the issue @kappelmann linked to (the quot.sound with French quotes) as an intentional cheat, seeing as it is very unlikely for a well-meaning Codewarrior to accidentally pass a Kata by stumbling upon it.

[kbuzzard]

For professional mathematicians using Lean, is there any situation where, for example, it would be useful to disallow one or more of the core axioms (propext, quot.sound, classical.choice), or, on the other hand, allow extra axioms on top of those three? If so, how often?

For an "ideal mathematician" like many of my colleagues in mathematics departments across the world, or budding "ideal mathematicians" like many of the students in these departments, propext, quot.sound and classical.choice are part of the axioms of mathematics, and many of us have no idea why computer scientists spend so much time fussing about them because they are all well-known to be true, and are used without comment in 99% of the modern mathematical literature. Conversely, the concept of adding a new axiom would be abhorrent to many of us, because we have all the axioms we need right now.

On the other hand, any computer scientist would point out that whether or not we mathematicians need those axioms would very much depend on the kind of question we are working on, and they would urge us to think about whether some of our proofs could be constructive. My experience is that this might be an issue as far as formalisation is concerned, but it is a question which is of no interest to an "ideal mathematician". Speaking as a mathematician I would hence (a) allow all assumptions of these three axioms (b) allow no more axioms other than these (c) not even mention this fact, assuming that mathematicians will be working under the assumption that they are allowed to do what they would call "normal mathematics".

However this does lead to the question of what kind of questions will be asked on code wars.

[DonaldKellett]

@kbuzzard Thanks for your input!

Speaking as a mathematician I would hence (a) allow all assumptions of these three axioms (b) allow no more axioms other than these (c) not even mention this fact, assuming that mathematicians will be working under the assumption that they are allowed to do what they would call "normal mathematics".

Amazing - this means that we (at Codewars) can take the simplistic approach of just accepting these 3 axioms and rejecting everything else all of the time instead of spending time figuring out how to support a dedicated testing framework with customization features and such.

However this does lead to the question of what kind of questions will be asked on code wars.

Since you are the target audience, we are looking forward to undergraduate and/or masters level questions on pure mathematics contributed by mathematicians (or budding mathematicians) like you.

[DonaldKellett]

@kazk For the icon, we can probably just use the official logo and re-color it to suit Codewars' theme.

[kbuzzard]

. Since you are the target audience, we are looking forward to undergraduate and/or masters level questions on pure mathematics contributed by mathematicians (or budding mathematicians) like you.

Did you ever take a look at Maths challenges for the lean curious? https://github.com/kbuzzard/xena/blob/master/Maths_Challenges/challenges.md I just decided today that I was going to stop prioritising that list because nobody ever seemed to talk about it. The natural number game just caught on independently but the challenges never did. I have loads more ideas. —

…

You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#773>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHTEHM7MVZQFMAARWMZLVOLRDPTPBANCNFSM4JIKC77Q> .

[kazk]

@DonaldKellett I just found the explanations for each kataN/ at the bottom of the README. I've got them running locally so I should be able to work from here by inspecting the outputs and how it fails.

leanchecker seems to take a while even for these examples (I guess it's checking a lot already since the output contains checked 9218 declarations). I hope the actual challenges doesn't take too much longer than these.

[kazk]

For the icon, I'll need more clean/simple SVG with just LEAN.

[DonaldKellett]

For the icon, I'll need more clean/simple SVG with just LEAN.

Maybe we could modify the official logo to have "LƎ" on top of "ⱯN" like what we initially did for Agda?

[DonaldKellett]

Without leanchecker for now?

Yeah, I think we should go without leanchecker since it really slows things down and we didn't use coqchk for Coq anyway so I don't see why we need to use leanchecker for Lean. It'll allow some metaprogramming loopholes as a few mentioned here but as I said, as long as solvers cannot accidentally solve a Kata by blindly stumbling on them then we can just treat it as a runner cheat and apply the usual punishments to anyone found abusing them.

[DonaldKellett]

It's been two weeks since there has been any activity in this issue ticket, but the 6/6 in the checklist would suggest that Lean support for Codewars is ready to go. @kazk Is there anything in particular (e.g. switching back to #print axioms method) holding this back?

Also I should note that a lot has happened in the Lean community in the meantime and the Lean community version is now 3.7.2. From what I get in the Zulip chat, the last official version of Lean (3.4.2) isn't really in use anymore so maybe we should consider supporting Lean v3.7.2 instead (or at least support it in addition to 3.4.2). For Lean v3.7+, they have new tooling which I've heard improves the workflow.

[kazk]

Is there anything in particular (e.g. switching back to #print axioms method) holding this back?

Yeah, can you update your examples?
This is delayed because I just haven't had the time to work on, but that will definitely help me.

we should consider supporting Lean v3.7.2 instead (or at least support it in addition to 3.4.2)

OK, I'll try using 3.7.2 instead. I wouldn't want to have two language versions unnecessarily (we usually do because there's existing contents waiting to be updated).

[kbuzzard]

My impression is that within a few weeks it'll be 3.8.1 and it's basically not going to stop. See leanprover-community/lean#160 for example.

…

On Fri, 27 Mar 2020 at 17:28, kazk ***@***.***> wrote: Is there anything in particular (e.g. switching back to #print axioms method) holding this back? Yeah, can you update your examples? This is delayed because I just haven't had the time to work on, but that will definitely help me. we should consider supporting Lean v3.7.2 instead (or at least support it in addition to 3.4.2) OK, I'll try using 3.7.2 instead. I wouldn't want to have two language versions unnecessarily (we usually do because there's existing contents waiting to be updated). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#773 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHTEHM6BYWFENSZIO53DYK3RJTO2JANCNFSM4JIKC77Q> .

[kazk]

We're obviously not going to keep adding every new Lean 3.x versions released. Just like any other languages.

Is Lean versioning semantic? Or does it contain breaking changes between minor version bumps (3.7 -> 3.8)?

Just to be clear, we can support 2 versions at the same time. And add new version when all the challenges are updated to the newer version and removing the older version. I just don't want to have 2 versions right now when we don't even have the reason to.

[vvs-]

Is Lean versioning semantic? Or does it contain breaking changes between minor version bumps (3.7 -> 3.8)?

I think it was when it was supported by Microsoft. Apparently community version is not as 3.6.0 is not backwards compatible. One suggestion was to rename it to avoid version clash with Lean4. I think that calling current community version Lean3 3.7.2 has its merits.

[DonaldKellett]

Yeah, can you update your examples?

This is delayed because I just haven't had the time to work on, but that will definitely help me.

I have to prepare for my midterms over the next two weeks or so but I'll see if I can squeeze a bit of free time to start looking into Lean 3.7.2 and update the examples accordingly.

[DonaldKellett]

The examples have been updated to use Lean3 v3.7.2.

[kazk]

@DonaldKellett I should be able to deploy Lean 3.7 on Codewars early next week. Your example helped a lot, thanks!

[kazk]

Deployed Lean support. See @DonaldKellett's examples for how it works.

Consider this alpha release. Please try it and let me know.

[DonaldKellett]

Nice! I will probably start translating some existing content into Lean3 (and author a few new Kata) once my midterms are over.

In the meantime, I noticed that the language was just called "Lean" on Codewars and think that it would be better to call it "Lean3" instead, considering that 1) we're currently using a community version and 2) Lean4 is basically considered a completely separate project from Lean3. I have already renamed Lean to Lean3 in the wiki accordingly.

[kazk]

Isn't the project still called Lean? The new project is called Lean4, but the older (but still actively developed) one is still Lean, isn't it? Reminds me of Perl and Perl6 confusion that lead to renaming to Raku.

[vvs-]

I quote from Lean4 readme:

We are currently developing Lean 4. Lean 3 is still the latest official release.

This is ambiguous because you can interpret the number as just the software release number. Calling it Lean3 or Lean4 is less ambiguous because in this case it's already part of a language name. There never was official statement about this and it remains a matter of personal preference, of course.

[alexjbest]

As lean 4 is under development (but not released) and will likely replace lean 3 in all instances (with some modifications) when it is released, I don't see why just calling it Lean and changing to Lean 4 when it is out and stable like everyone else. The same thing happened with Lean 2 -> Lean 3. There will be a fair amount work to port mathlib to Lean 4 when it comes out so it wont be instant, but the impression I have is that Lean 4 really is the next upgraded (completely rewritten) version.

[kazk]

Is there any plans to automate Lean 3 to 4 upgrade (e.g., some tool to automatically fix breaking changes)? Also, what happens to Lean 3 once Lean 4 becomes the official release?

These are kind of important for us because we track progress per language. If converting Lean 3 to Lean 4 is possible (and considered the same language), we should have one language Lean and support these as language versions. If Lean 4 is going to replace Lean 3, I'd rather have these as language versions as well because I wouldn't want to keep Lean 3 as a language forever after Lean 4 replaced it.

As lean 4 is under development (but not released) and will likely replace lean 3 in all instances (with some modifications) when it is released
There will be a fair amount work to port mathlib to Lean 4 when it comes out

Sounds like we should just have language Lean and add version 4 when it becomes ready and port the challenges.

[vvs-]

Is there any plans to automate Lean 3 to 4 upgrade (e.g., some tool to automatically fix breaking changes)?

The only thing we know at this time is what said in Lean4 papers and public events: that developers are hoping to use its new macro feature to implement some parts of Lean3 language inside Lean4. But there are many differences including but not limited to: naming conventions, different syntax, different core library...

Also, what happens to Lean 3 once Lean 4 becomes the official release?

Good question for Lean3 development team members. Seems that naming is not the thing they are most concerned with. But this is already beginning to create some problems in the long term. Breaking semantic versioning was just one of them, IMHO.

[DonaldKellett]

@kazk I've just sent you an updated version of my 0.999... = 1 example by email, may you please run and time it again to confirm my results? I've just looked into publishing this Kata but am getting consistent timeouts even under the extended 16-second limit. Running lean SolutionTest.lean --profile on my local machine gives the following cumulative profiling stats:

cumulative profiling times:
	compilation 2.08ms
	decl post-processing 11ms
	elaboration 10s
	elaboration: tactic compilation 80.3ms
	elaboration: tactic execution 7.54s
	parsing 2.72s
	type checking 1.43ms

[kazk]

The output for the version you sent me:

cumulative profiling times:
	compilation 0.262ms
	decl post-processing 1.71ms
	elaboration 5.86s
	elaboration: tactic compilation 53.7ms
	elaboration: tactic execution 5.24s
	parsing 1.71s
	type checking 0.734ms

This took about 13s. The Runner's wall time was 16176ms.

I've been using Kevin Buzzard's version as a reference:

cumulative profiling times:
	compilation 0.155ms
	decl post-processing 0.772ms
	elaboration 1.31s
	elaboration: tactic compilation 7.34ms
	elaboration: tactic execution 1.18s
	parsing 201ms
	type checking 1.17ms

This took about 10s. The Runner's wall time was 12259ms.

These are the numbers on my computer and it seems like Kevin's version have 14-16s walltime on Codewars.

I'll be increasing the amount of memory allowed in the container (unrelated to Lean) so that might help. If not, I'll consider increasing the time limit little bit.

[DonaldKellett]

Sounds good to me. Ping me when the memory limit is changed on Codewars so I may test my 0.999... = 1 draft Kata again and see if that helps.

[Voileexperiments]

I've just finishing setting up my local leanprover environment and it seems that CW has some default imports. For example, for this solution, it doesn't work until I add import data.real.basic to the code.

Are there additional setup that hasn't been documented yet?

[DonaldKellett]

Lean3 is in active development so they make breaking changes regularly in mathlib (and sometimes in core as well). You might want to check in your leanpkg.toml that your project uses Lean 3.7.2 with the exact mathlib commit as stated in the Wiki. If not, then editing your leanpkg.toml locally and running leanproject build may help.

[Voileexperiments]

??? I already had that setup according to this, hence why it works after I added import data.real.basic. It's still missing the import in the end though, that's why I'm asking if there are any default imports not mentioned in the CW environment docs.

[kazk]

@Voileexperiments
There shouldn't be any default imports. Runner only does lean SolutionTest.lean --json.

This is the exact leanpkg.toml used by Runner:

[package]
name = "lean-challenge"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ecdb13831d4671eb304c41e78adb5b280c2fc365"}

We do the following to set up the project:

# Get mathlib olean files
leanproject get-mathlib-cache
# Check timestamps are correct
leanproject check