Lean
#
Version#
Test FrameworksNone
#
Allowed axiomsAs 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 SupportUnfortunately, 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 environmentFollow the instructions over at leanprover-community to install the complete Lean development environment locally on your machine (if you haven't done so already). Then:
On your command line, run
leanproject new kata
. This creates a folderkata
with the latest Lean community version and the corresponding pre-compiled mathlibOn your command line, run
cd kata
to enter thekata
folder.In your browser, go to the kata you plan to solve (e.g. Theorem proving hello world), choose Lean as the language you want to train on and click on the "Train" / "Train Again" button to enter the kata trainer.
In your browser, near the top center-right of the trainer, select a language version by clicking on it and make note of it. For example, in Theorem proving hello world, both "3.7.2 ecdb138" and "3.11.0 51e2b4c" are enabled. Ideally, we should select the more recent language version "3.11.0 51e2b4c", but for demonstration purposes here, we will go with the older version "3.7.2 ecdb138":
In a text editor of your choice (e.g. VSCode or Atom), open your
leanpkg.toml
file: Remember we selected "3.7.2 ecdb138" on Codewars for the Lean language version. This means that our desired Lean version is v3.7.2, with a mathlib commit whose id starts with "ecdb138". In this case, the full id of the mathlib commit is ecdb13831d4671eb304c41e78adb5b280c2fc365. So on line 4 in the screenshot above, edit thelean_version
to 3.7.2, and on line 8 in the screenshot above, edit therev
field ofmathlib
to "ecdb13831d4671eb304c41e78adb5b280c2fc365" and save your changes:Using your text editor or otherwise, populate
kata/src
with the following files:Preloaded.lean
: The Preloaded section of the kata, if exists. Usually, kata authors will display the full source code of the Preloaded section in the kata description so just copy-paste that intoPreloaded.lean
Solution.lean
: Your solution to this kataSolutionTest.lean
: The (Sample) Test Cases for this kata
On your command line, run
leanproject get-mathlib-cache && leanproject build
Now you should be good to go. When solving the kata locally, remember not to modify Preloaded.lean
or SolutionTest.lean
- the only file you should be working on is Solution.lean
. Then, once your project builds without any errors or sorries, copy-paste the full text of Solution.lean
back to the kata trainer and hit the "Attempt" button. Given that your solution does not take more than 20s to compile, you should see the blue "Attempt" button turn into a green "Submit" button. Hit the green button and you've solved the kata!
#
Timeout20 seconds
#
PackagesNone
#
ServicesNone
#
Language IDlean