Language Lean

Status

Beta

Versions

3.7.2 with mathlib (commit: ecdb13831d4671eb304c41e78adb5b280c2fc365)

Test Frameworks

None

Allowed axioms

As is usual in mathematical practice, you may freely invoke classical / non-computable principles in your Lean proofs without reservation, e.g. excluded middle, axiom of choice, etc. If constructivism / computability is a major concern then please consider switching to Coq / Idris / Agda instead.

Interactive Proof Editing Support

Unfortunately, the Codewars environment does not support the interactive development of Lean proofs. The current recommended method of solving a Kata is by copying the relevant code snippets onto your local machine and developing your solution locally.

Setting up your local environment

1. Install elan

2. Run pip3 install mathlibtools, with sudo if necessary

3. Run leanproject new kata. This automatically creates a Lean3 project in kata/ with the latest Lean3 community version (3.7.2 at the time of writing) and the corresponding pre-compiled mathlib

4. Populate kata/src/ with the following Lean files:

   • Preloaded.lean: The Preloaded section of the Kata
   • Solution.lean: Your solution to this Kata
   • SolutionTest.lean: The (Sample) Test Cases for this Kata

   You should not modify Preloaded.lean or SolutionTest.lean when developing your solution locally, since you are not allowed to modify them on Codewars upon submission. To test your submission, open your command line, cd to kata/src/ and run lean SolutionTest.lean. A passing solution should only see one or more of the following lines (in any order, appearing any number of times) printed out to the console:

   • no axioms
   • propext
   • quot.sound
   • classical.choice

Timeout

16 seconds

Packages

None

Services

None