Study note
Natural Number Game
Properties
- Type
- Blogs
- Status
- 待读
- Domain
- Math
- Category
- 代数几何、Lean 与可视化
- Source
- adam.math.hhu.de
- Vault note
library/articles/math/Natural-Number-Game-5974b7b45e15bc07.md
Summary
从零开始在浏览器中证明自然数的基本性质，通过逐关解锁 `rfl`、`rw`、`simp`、`apply`、归纳等 tactic，实时观察 goal 与 local context 的变化。
Highlights
无需安装环境，反馈即时；适合先形成“读 proof state -> 选择 tactic -> 检查新目标”的基本循环。
Notes
用自然数证明闯关进入 Lean 4。
Comments
Loading comments...