Tutorials:
- Glimpse.
- Natural number game. (I am playing it.)
- Theorem Proving.
- Functional programming.
Others:
- Terry Tao's blog. And his talk.
- A HOL4 user on Weibo.
- Slides that provide a good general picture.
- Links from the official.
- Quantum information theorem library, e.g., lean-quantum.
- With AI. (Can it solve some QI math problems?)
- LeanCopilot.
- Meta's public AI model that solved 10 International Mathematical Olympiad problems. News.