Original article
The Future of Mathematics? - YouTube
Kevin Buzzard’s Blog
https://xenaproject.wordpress.com/
Source code
https://github.com/leanprover/lean
Emacs mode
https://github.com/leanprover/lean-mode
Lean blog (Microsoft Research)
http://leanprover.github.io/

Work in progress

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17  Lean [#Microsoft research] [programming language] A theorem prover and programming language. It is based on the Calculus of Constructions with inductive types. Lean has a number of features that differentiate it from other interactive theorem provers. Lean can be compiled to JavaScript and accessed in a web browser. It has native support for Unicode symbols.

He thinks it’s going to turn the entire world upside-down.

He thinks it’s the future of maths.

## Learning Lean

https://xenaproject.wordpress.com/category/learning-lean/

## Learning Lean by example

https://xenaproject.wordpress.com/2018/12/30/learning-lean-by-example/

## Install Lean

 1 2 3 4 5 6 7 8  Lean 4 Lean 4 is under development. There are no official releases yet. Lean 3 These are the official releases of Lean 3. For the extended community version of Lean 3, please see leanprover-community/lean.

https://github.com/leanprover/lean/releases/tag/v3.4.2

### Installing Lean

 1  cd "$DUMP/programs"; wget "https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz"  1  lean --help Lean (version 3.4.2, commit cbd2b6686ddb, Release) Miscellaneous: --help -h display this message --version -v display version number --githash display the git commit hash number used to build this binary --run executes the 'main' definition --doc=file -r generate module documentation based on module doc strings --make create olean files --recursive recursively find *.lean files in directory arguments --trust=num -t trust level (default: max) 0 means do not trust any macro, and type check all imported modules --quiet -q do not print verbose messages --memory=num -M maximum amount of memory that should be used by Lean (in megabytes) --timeout=num -T maximum number of memory allocations per task this is a deterministic way of interrupting long running tasks --threads=num -j number of threads used to process lean files --tstack=num -s thread stack size in Kb --deps just print dependencies of a Lean input --path display the path used for finding Lean libraries and extensions --json print JSON-formatted structured error messages --server start lean in server mode --server=file start lean in server mode, redirecting standard input from the specified file (for debugging) --profile display elaboration/type checking time for each definition/theorem -D name=value set a configuration option (see set_option command) Exporting data: --export=file -E export final environment as textual low-level file --only-export=decl_name only export the specified declaration (+ dependencies) --test-suite capture output and status code from each input file$f in $f.produced and$f.status, respectively


## Using CTest

 1  man +/"ctest - CTest Command-Line Reference" "ctest(1)"
  1 2 3 4 5 6 7 8 9 10 11  NAME ctest - CTest Command-Line Reference SYNOPSIS ctest [] DESCRIPTION The "ctest" executable is the CMake test driver program. CMake-generated build trees created for projects that use the ENABLE_TESTING and ADD_TEST commands have testing support. This program will run the tests and report results.

## Some examples

 1  cd "$MYGIT/leanprover/lean"; tp find-here-path "*exampl*" tmp/debugger_example.lean tests/lean/example_false.lean tests/lean/example_false.lean.expected.out tests/lean/run/untrusted_examples.lean tests/lean/run/example1.lean tests/lean/run/noncomputable_example.lean tests/lean/fail/example.lean  ### Fasle  1 2 3 4 5  open expr tactic example : false := by do n ← mk_fresh_name, apply (local_const n n binder_info.default (const false [])) /tmp/babel-WZwsIE/generic-XNA4Z0:3:0: error: failed to add declaration to environment, it contains local constants  ### 584a.lean   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19  universe variables u variables (A : Type u) [H : inhabited A] (x : A) include H definition foo := x #check foo -- A and x are explicit variables {A x} definition foo' := x #check @foo' -- A is explicit, x is implicit open nat #check foo nat 10 definition test : foo' = (10:nat) := rfl set_option pp.implicit true #print test foo : Π (A : Type u_1) [H : inhabited A], A → A foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ def test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 := λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))  ## lean by example   1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114  -- Inductive propositions. -- Example 1: even numbers. -- inductive definition of "is_even" predicate on the real numbers inductive is_even : ℕ → Prop | even0 : is_even 0 | evenSS : ∀ n : ℕ, is_even n → is_even (n + 2) open is_even theorem four_is_even : is_even 4 := begin -- goal now is_even 4 apply evenSS, -- goal now is_even 2 apply evenSS, -- goal now is_even 0 exact even0 end -- can do it with functions too theorem six_is_even : is_even 6 := evenSS 4$ evenSS 2 $evenSS 0 even0 theorem one_is_not_even : ¬ (is_even 1) := begin intro H, -- H : is_even 1 -- clearly H can not have been proved using either even0 or evenSS -- so when we do this cases H, -- there are no cases left, so the proof is over! end -- cases can also be used to pull down higher odd numbers theorem five_is_not_even : ¬ (is_even 5) := begin intro H5, cases H5 with _ H3, cases H3 with _ H1, cases H1, end -- example of usage lemma even_iff_SS_even (n : ℕ) : is_even n ↔ is_even (n + 2) := begin split, { -- easy way exact evenSS n, }, -- other way a bit trickier intro HSSn, cases HSSn with _ Hn, assumption end -- Example 2: the Collatz conjecture. /-- collatz n means the collatz conjecture is true for n -/ inductive collatz : ℕ → Prop | coll0 : collatz 0 | coll1 : collatz 1 | coll_even : ∀ n : ℕ, collatz n → collatz (2 * n) | coll_odd : ∀ n : ℕ , collatz (6 * n + 4) → collatz (2 * n + 1) open collatz theorem coll10 : collatz 10 := begin apply coll_even 5, apply coll_odd 2, apply coll_even 8, apply coll_even 4, apply coll_even 2, apply coll_even 1, apply coll1 end theorem coll10' : collatz 10 := coll_even 5$ coll_odd 2 $coll_even 8$ coll_even 4 $coll_even 2$ coll_even 1 coll1 -- if m is odd then 3m+1 is always even, so we can go from m=2n+1 to 6n+4 and then to 3n+2 in one step. lemma coll_odd' (n : ℕ) : collatz (3 * n + 2) → collatz (2 * n + 1) := begin intro H3n2, apply coll_odd, -- unfortunately applying coll_even will tell us about collatz (2 * (3 * n + 2)) -- rather than collatz (6 * n + 4), so let's fix this rw (show 6 * n + 4 = 2 * (3 * n + 2), by rw [mul_add,←mul_assoc];refl), -- with tactic.ring imported from mathlib this line could just be -- rw (show 6 * n + 4 = 2 * (3 * n + 2), by ring), apply coll_even, assumption end -- now we can go a bit quicker theorem coll10'' : collatz 10 := begin apply coll_even 5, apply coll_odd' 2, apply coll_even 4, apply coll_even 2, apply coll_even 1, apply coll1 end -- Of course one should really be using a home-grown tactic to figure out which -- of coll_even, coll_odd and coll1 to apply next. /- this is the Collatz conjecture -/ -- theorem collatz_conjecture : ∀ n : ℕ, collatz n := sorry -- Nobody knows how to prove this.