Terence Tao用AI打造逻辑证明游戏
Lean Grimoire
我最近利用现代编程代理，将2018年制作的交互式逻辑教科书“QED”进行了现代化重构，并将其命名为“Lean Grimoire”。这个项目旨在通过“ Crafting Game”的形式教授命题逻辑和一阶逻辑，用户需要运用各种逻辑规则，从给定假设推导出目标结论。新版本不仅增加了显示当前游戏状态对应的Lean证明进度的功能，还趣味性地加入了“幻想模式”，将数学语句转化为“药水”，数学表达式变为“卷轴”。我希望能通过众人的试玩测试，让这款应用成为学习逻辑证明和Lean定理证明器的有效工具。
该教科书的目的是以“制作游戏”的形式教授命题逻辑和一阶逻辑，玩家需要应用各种逻辑规则，从一组给定的假设推导出期望的结论。
- torben-friis
这教育游戏做得一团糟。
抱歉这么消极，但那个充满大模型味道的介绍简直让人难以读懂，而那些操作说明看起来就像是一份没写完的个人 Obsidian 笔记。
出自 Tao 之手实在有点奇怪，我记得他写的数学笔记一向通俗易懂、文笔流畅。