TODO list

[RexWzh]

TODO

• Lean4Game 使用教程
• 游戏版本的 A Glimpse Of Lean 文档
• LeanDojo 使用教程及源码解读
• 其他工具教程

Lean4Game

用 lean4game 部署 Lean 4 游戏，比如 NNG4，域名已备案，放在了国内服务器上：

https://nng4.lookeng.cn

由于 leanprover.cn 是组织性质的账号，在国内备案非常麻烦，只能解析到国外服务器：

https://nng4.leanprover.cn

后续打算写点小游戏，比如个人的专业背景，李理论。

当前，A Glimpse Of Lean 的习题很适合以游戏形式的教学，比纯看翻译更有价值，可以先从这里开始：https://github.com/Lean-zh/GlimpseToGame

LeanDojo

lean-dojo 提供了环境交互和信息提取的工具。

当前工具只支持引用 Github 仓库，过去一年了，这个问题竟然还没人解决。。。最近抽时间改下，顺便给仓库提个 PR。（已解决，详见 2.1.0 版本）

其他

其他工具，比如 llmstep, LeanCopilot 也可以出个教程。这几个都是去年的工作了，今年应该还有一些值得实践的内容。