在线使用Lean4：https://leanprover-community.github.io/lean-web-editor/
文档
https://subfish-zhou.github.io/theorem_proving_in_lean4_zh_CN/propositions_and_proofs.html
https://leanprover-community.github.io/mathematics_in_lean/index.html
https://www.leanprover.cn/GlimpseOfLean/
https://www.leanprover.cn/fp-lean-zh/title.html
https://leanprover.github.io/functional_programming_in_lean/
https://lean-lang.org/lean4/doc
https://hrmacbeth.github.io/math2001/index.html
https://github.com/leanprover-community/lean4-metaprogramming-book
http://adam.chlipala.net/frap/
游戏
https://adam.math.hhu.de/
https://www.codewars.com/
视频
https://www.bilibili.com/video/BV1fG4y1W7p4
https://www.bilibili.com/video/BV12m4y1x7CA
https://www.bilibili.com/video/BV16W4y1U7BT
https://www.bilibili.com/video/BV1BM4y1o7U5
https://www.bilibili.com/video/BV1sA411x7QK
https://www.bilibili.com/video/BV1wU4y1475g
https://www.bilibili.com/cheese/play/ss18364?bsource=link_copy
https://www.bilibili.com/video/BV1Lk4y1D7uC
https://www.bilibili.com/video/BV1oz4y1D7ws
https://www.bilibili.com/video/BV1Nc411m7z1
https://www.bilibili.com/video/BV1fN411g7Dv
https://www.bilibili.com/video/BV1K7411B7is
https://www.bilibili.com/video/BV1QZ4y1a74J
https://www.bilibili.com/video/BV1tA41127Lm
https://www.bilibili.com/video/BV1ix421Q7KR
数学的形式化——定理证明语言Lean入门 (课程介绍)
https://its.westlake.edu.cn/info/1017/1942.htm
更多材料可参考：https://leanprover-community.github.io
探索 Lean Math Workshop：一个现代化的数学学习和研究工具
项目地址:https://gitcode.com/yuma-mizuno/lean-math-workshop
Lean Zulip chat 链接：https://leanprover.zulipchat.com/