故事 一次超高能粒子流击中了一艘正在前往系外行星的巨型星际飞船，导致导航系统的存储器发生灾难性损坏。 为了应对危机，飞船的管理 AI 将两名乘客从冷冻休眠中唤醒。 一位是咖啡店店员优子（Yuko）。 另一位是拉面店服务员兼吉他手健二（Kenji）。 两人对星际飞船或计算机系统一窍不通，但 AI 却无情地宣布： “我彻底忘记了所有关于数学的知识！” AI 真的什么都不记得了——甚至连“0”或“1”的含义都忘了。 没有数学，就无法进行导航。 一个奇怪的终端出现在困惑的两人面前，上面充满了难以理解的符号和令人费解的逻辑。他们唯一的盟友是一个猫形的紧急响应机器人。 “证明给我看！” 优子和健二能否恢复系统？为什么被唤醒的是这两个人？…
故事
一次超高能粒子流击中了一艘正在前往系外行星的巨型星际飞船，导致导航系统的存储器发生灾难性损坏。
为了应对危机，飞船的管理 AI 将两名乘客从冷冻休眠中唤醒。
一位是咖啡店店员优子（Yuko）。
另一位是拉面店服务员兼吉他手健二（Kenji）。
两人对星际飞船或计算机系统一窍不通，但 AI 却无情地宣布：
“我彻底忘记了所有关于数学的知识！”
AI 真的什么都不记得了——甚至连“0”或“1”的含义都忘了。
没有数学，就无法进行导航。
一个奇怪的终端出现在困惑的两人面前，上面充满了难以理解的符号和令人费解的逻辑。他们唯一的盟友是一个猫形的紧急响应机器人。
“证明给我看！”
优子和健二能否恢复系统？为什么被唤醒的是这两个人？飞船及其乘客将面临怎样的命运？
定理证明谜题
《Glass Beads》是一款谜题小说游戏，你需要以解谜的形式证明数学定理。
由于 AI 忘记了所有数学痕迹——甚至包括数字 0 和 1 以及加法和乘法等基本运算——你必须从零开始， painstakingly 重建数学概念。
这些定理本身的含义简单到小学生都能理解，但要给出严谨的逐步证明却绝非易事。
依靠猫型机器人的细致讲解，解决谜题，揭开星际飞船及其背后的故事之谜！
深入探索
游戏中的谜题旨在提供柯里-霍华德同构（Curry–Howard correspondence）的实践体验。
基于马丁-洛夫直觉类型论（Martin-Löf's Intuitionistic Type Theory, ITT）的依赖类型系统，以及建立在皮亚诺算术基础上的理论，你将构造性地证明初等数论中的定理。
你将从自然数的基本算术性质证明开始，随后迎接基于这些证明构建的应用挑战，例如字符串操作问题。
