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.

The latest version is archived.

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

https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz

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 [<options>]

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.