Documentation

• LeanDoc
• Complete list of Lean4 tactics
• Course on SAT, SMT, ITP using Lean (Book)
• Lean3 Tactics in Lean4
• Different ways of search for theorems or functions

Projects

• Maze
• KArray
• NumLean
• Blake3 Hasher
• Advent of Code in Lean 4
• Mini Redis

Tips

dbgTrace "hello" $ fun _ => Will print hello before evaluating an expression