学Lean像打怪？这个仓库想让形式化证明不再劝退

每次看到"依赖类型论"四个字，我就条件反射地打退堂鼓——Lean的学习曲线太陡了。但有个叫Adam的人把这件事想成了游戏设计问题：能不能把定理证明拆成一个个关卡，让人在"通关"中不知不觉掌握归纳、量词、类型匹配？他的仓库Lean Game Server正是干这个的，把Lean的交互式证明体验包装成一套教学关卡集。我觉得这思路对，但HN上只有1个赞、1条评论也说明问题：形式化验证社区依然太小众，连游戏化都带不动热度。不过，如果让数学系学生像刷LeetCode一样刷Lean题型，入门门槛或许真能降下来。

原文：Lean Game Server: A repo of learning games for Lean · 来源：Hacker News