Digest Lean 4 materials

[utensil]

• http://outlace.com/Lean_part_1.html
• https://typista.org/lean-for-scala-programmers/
• https://icerm.brown.edu/video_archive/?play=2906

[utensil]

• 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
  • https://plfa.github.io/
  • https://github.com/plfa/plfl
• 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]

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]

Lean Phrase book: https://docs.google.com/spreadsheets/u/0/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/htmlview