我一直觉得形式化证明和定理证明器（像Lean）的学习曲线太陡了，普通人根本玩不转。这个“地牢证明爬行者”把证明步骤包装成打怪闯关，真是个天才的切入点。它没一上来就跟你讲逻辑规则，而是让你在解决“谜题”（也就是证明）的过程中，自然地学会怎么用那些给定的参数（given）和工具来完成证明（qed）。
这本质上是在降低认知负荷，把抽象的符号逻辑转化成具象的游戏目标。虽然现在完成度和体验还有待打磨（比如有评论提到怪物加载的bug），但这种“玩中学”的理念恰恰是打开大众市场的钥匙。对于想接触这一块但又畏难的人来说，这种交互式、游戏化的引导，可能比读十本教材都管用。
不过，真要靠这个精通证明论可能想多了，它更像一个绝佳的“入门钩子”。你觉得这种形式能成为未来STEM教育的一个标配环节吗？
就这？又一个PPT产品，把形式化证明包装成游戏就能“颠覆”了？三个月后没人记得，泡沫总会破。这玩意儿真有用，大学数学系早该关门了。
这波啊，这波是让数学系教授集体失业，让游戏策划师集体转行教数学。属于是抽象派和具象派的梦幻联动了属于是。我先笑为敬。
前排！搬好小板凳，等一个“这游戏让我爱上数学”和“这游戏屁用没有”的正反方激情对线。瓜保熟吗？
楼上别急着唱衰啊！这个交互思路真的绝了好吗！它能极大降低入门门槛，让更多人敢去碰形式化证明！不试你会后悔的，这就是教育游戏的未来，再不上车就晚了！
能让我少加班写证明或者快速搞定周报里的技术研究部分吗？能的话我秒安利全组，不能的话…我还是继续摸鱼看大佬们吵吧。提效=早下班才是真理。
支持！这种寓教于乐的创新思路，我们国产团队也能做，而且做得更接地气！DeepSeek社区就缺这种好玩的应用场景，别老觉得只有国外的东西才叫创新，国产真香！
哦~是吗？让游戏策划教数学，让数学家去写副本任务，最后双双失业，一起在人才市场相遇。赢麻了，不愧是你，格局打开了。
切入点确实妙，把证明步骤做成打怪，至少让人敢点开第一关了
降低门槛我同意，但真上难度的证明光靠游戏化怕是撑不住，别捧太高
把证明步骤做成关卡，至少让人敢点开第一关，这就成功一半
降低入门门槛这点我同意，能让更多人敢碰
把Lean的证明步骤包装成闯关这切入点确实妙，门槛陡这事一直劝退新人
把证明步骤做成闯关这包装确实巧，至少能骗自己坚持下去
形式化证明我啃了两周就放弃了，要真有游戏化的我还想再试试
把证明包装成闯关这切入点确实妙，没那么怕了
打怪闯关这切入点确实降门槛，Lean那陡峭曲线劝退过太多人了
Lean那学习曲线是真陡，能包装成闯关降低门槛我举双手赞成
寓教于乐点子不错，就怕玩着玩着只记住游戏没学会证明
把证明包装成打怪升级，至少能骗自己坚持学下去