由于各自不同的原因，发现大家这个学期都开始学习起 Lean 了起来，我也不能免俗囧。L∃∀N 一看 logo 就很帅，有点 DUNE 的设计感有没有？
感觉首要工作是先复习一下 Haskell，这样也不必中途翻阅语法手册。显然 Lean4 从 Haskell 里借鉴了相当多的语法和设计思想，说来惭愧，虽然我之前试图用 Haskell 刷刷题，但是总是感觉不得要领，被复杂度卡的死死的囧不得不中途切回 cpp 艹。fingertree 什么的也看的云里雾里，感觉还是我的姿势水平不够，还需特别努力！
然后初学 Lean 我是建议先看 Mathematics in Lean，本书直接使用 mathlib，让你不必过早的被细节劝退，又可以顺便复习一下熟悉的数学知识（初等数论她不香吗，天天学代数人都学傻了）。而且还提供对应的 Github 仓库，可以 step-by-step 边看别改。Lean 不能没有 mathlib，就像是 cpp 不能没有 std，西方不能没有耶路撒冷？
（目前感觉这语言除了优化不行哪哪都还可以？）
再然后感觉可以试试写点题目，比如可以试试先证明静态直径算法？
学习
- Lean (proof assistant), Wikipedia
- https://leanprover-community.github.io/learn.html
- Lean Focused Research Organization
- Theorem Proving in Lean
- Mathematics in Lean
- Type Checking in Lean 4
- Functional Programming in Lean
- https://lean-lang.org/lean4/doc/
习题
研究
- Peano: Learning Formal Mathematical Reasoning
- Proof Artifact Co-training for Theorem Proving with Language Models
- Generative Language Modeling for Automated Theorem Proving
- Solving (some) formal math olympiad problems
- LeanDojo: Theorem Proving in Lean using Language Models
- 千里冰封 – Canonical定理证明器 -20240508-（内部报告，非公开演讲，仅限爱好者交流）
