- http://outlace.com/Lean_part_1.html
- https://typista.org/lean-for-scala-programmers/
- https://icerm.brown.edu/video_archive/?play=2906
utensil commented at 2023-08-30 11:05:
- https://leanprover.github.io/theorem_proving_in_lean4/
- https://github.com/leanprover-community/lean4-metaprogramming-book
- Lean series on writing tactics
- Programming Language Foundations in Lean 4
- How To Prove It With Lean - authored with Quarto
- The mechanics of proof
- https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
- https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md
- https://github.com/bridgekat/filter-game#general-tips
- https://github.com/madvorak/lean3-tactic-lean4
- https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
- https://github.com/siddhartha-gadgil/proofs-and-programs-2023
- https://leanprover-community.github.io/contribute/naming.html
- https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention
- https://leanprover-community.github.io/extras/tactic_writing.html
- https://github.com/ianjauslin-rutgers/pythagoras4/
- https://ericwieser.me/
utensil commented at 2023-11-28 14:18:
Informalize:
- https://leanprover-community.github.io/format_lean/example/sandwich.html
- https://www.imo.universite-paris-saclay.fr/~patrick.massot/Examples/ContinuousFrom.html
15-815 Automated Theorem Proving: https://www.cs.cmu.edu/~fp/courses/99-atp/schedule.html
utensil commented at 2023-12-23 10:24:
Lean Phrase book: https://docs.google.com/spreadsheets/u/0/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/htmlview