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