Anything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.