Review of 'The Future of Mathematics? - YouTube'
- 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
|
|
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
|
|
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
|
|
|
|
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
|
|
|
|
Some examples
|
|
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
|
|
/tmp/babel-WZwsIE/generic-XNA4Z0:3:0: error: failed to add declaration to environment, it contains local constants
584a.lean
|
|
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
|
|
Thanks for reading!
If this article appears incomplete, it may be intentional. Try prompting for a continuation.
If this article appears incomplete, it may be intentional. Try prompting for a continuation.