lean4-tutorial
所属分类：lean
开发工具：Lean
文件大小：0KB
下载次数：0
上传日期：2024-02-13 14:06:15
上 传 者：
sh-1993
说明： 托马斯·亨辛格（Thomas Henzinger）课程的补充材料——每个计算机科学家都应该知道的形式主义
(Supplementary material for Thomas Henzinger s course Formalisms Every Computer Scientist Should Know)
文件列表:
ISTA/
LICENSE
lake-manifest.json
lakefile.lean
lean-toolchain
# Lean 4 tutorial
## Timeline
[2024-02-07](https://github.com/madvorak/lean4-tutorial/blob/master/ISTA/Class1.lean)
[2024-02-08](https://github.com/madvorak/lean4-tutorial/blob/master/ISTA/Class2.lean)
[2024-02-13](https://github.com/madvorak/lean4-tutorial/blob/master/ISTA/Class3.lean)
## How to Lean 4
### Setup Lean
[Minimalistic online IDE](https://github.com/madvorak/lean4-tutorial/blob/master/https://live.lean-lang.org/) (no installation needed; just copypaste the code and walk through the proof)
[Quickstart](https://github.com/madvorak/lean4-tutorial/blob/master/https://github.com/leanprover/lean4/blob/master/doc/quickstart.md)
[Official installation manual](https://github.com/madvorak/lean4-tutorial/blob/master/https://leanprover-community.github.io/get_started.html)
### Learn Lean
[Natural Number Game](https://github.com/madvorak/lean4-tutorial/blob/master/https://adam.math.hhu.de/#/g/hhu-adam/NNG4) (fun interactive tutorial by Kevin Buzzard et al.)
[Overview of basic tactics](https://github.com/madvorak/lean4-tutorial/blob/master/https://github.com/madvorak/lean4-tactics) (things you use in proofs, not definitions)
[Code from my minicourse](https://github.com/madvorak/lean4-tutorial/blob/master/https://github.com/madvorak/lean4-course) (took place at ISTA in 2023-09)
近期下载者：
相关文件：
收藏者：