MSE000 - 《数学超特急》中心页
暂定名为数学超特急的游戏，是速递三部中的第三部。
本游戏旨在通过结合Lean4的交互式策略证明器和Manim（数学动画引擎），类似于更为动画化的leangame，为一般的解谜游戏爱好者或者对数学有兴趣的高中生/非数学专业大学生/数学爱好者提供较为专业性的数学科普。通过使用Mathlib，以及将传统教科书中的题目转译成Lean形式，来提供多个数学领域的习题，供玩家游玩。
目前考虑的是完成开源的游戏框架。
游戏结构
为了阐述本游戏的结构，接下来我们需要引入概念：星球、卷、章节、题。
星球
星球包含了一个或多个DAG，由卷作为节点，卷之间的依赖关系作为有向边。类似于大学中一系列有前置要求的课程组成的一个培养方案（当然也可以只有少量的几个卷），星球可以由官方（作者）提供，或者由玩家自由创建（社区协助的模式下）。星球间是平行关系，没有依赖关系，玩家随时可以选取一个星球加载，并可以保存自己的星球进度。
对于星球内的卷排布顺序，作者在讨论后认为需要提供两种游玩顺序，以提供差异化的游玩体验，适合于不同需求的玩家：归纳序与认知序。
- 对于归纳序：提供公理，玩家证明定理，就是这么简单。玩家一步一个脚印，亲自打下现代数学大厦的每一块基石。类似于布尔巴基学派的教学方式，游玩难度较高，对于玩家的能力要求也较高，但是作者认为会更有成就感，且关卡不必排序，顺其自然即可。
- 对于认知序：从实际到抽象，类似于现实中的教学路径。虽然对于每一卷，玩家仍是在拥有公理的前提下进行定理证明，但是可以使用一些玩家没有证明过的卷中的代数结构/定理进行逃课，在之后的游戏中再回头证明。这个顺序游玩难度较低，对玩家也更为友好，但是需要设计顺序来引导玩家认知。
卷
卷类似于现实中大学的单门课程。卷包含串行的一系列章节，玩家需要达到一个章节的完成要求才能解锁其后继章节。初始章节（没有前继）在卷解锁的时候始终可用，最终章节完成后，整个卷完成。
在卷内，安装章节顺序，会逐步引入必要的公理，到卷的末尾玩家完成所有需要的定理的证明，确保玩家完全掌握了该卷的内容。
章节
章节类似于教课书内的章节（不过有可能会更短）。一个章节内可能会包含一些阅读内容、一些公理的解锁、一些策略（tactics）的解锁。一个章节大概率会包含（如不包含则是一个平凡的章节）数道题，题享有分值，玩家完成题后可以获得分值。在章节内获得分值大于等于章节分值需求且同时满足章节必要要求时，视作达到章节完成要求。
题
类似于现实中的题目，本游戏中的题有以下数种：证明题、计算题、构造题。
- 对于证明题，类似于leangame，不再赘述。
- 对于计算题，事实上我们考虑的是玩家证明表达式=答案，使用类似证明题的方式去处理。
- 对于构造题，玩家需要用给定的操作进行结构的构造，通过类似SPJ（Special Judge，一个专门的判定程序）的判定程序来判定玩家的构造是否满足题目要求。
一般而言，证明题是卷内的主要题型。为了玩家的游戏体验，题目会根据难度分成以下等级
- 基础题（下简称难度1，D1）
- 练习题（D2）
- 作业题（D3）
- 考试题（D4）
- 研究题（D5）
- 开放题（D6）
对任意章节，玩家需要完成所有D1题（或者说，D1题全部完成是章节的必要要求），以确保玩家对基本性质的掌握。D2~D4属于给予正分值的题，玩家需要积累分数来满足章节分值需求。其中D4等级的题目对一般玩家而言仅供挑战，一般不会出现在完成所有D2、D3题的情况下仍未满足分值要求。
D5题会从已经完成的Lean形式化证明摘取，玩家也许可以尝试去学习。
D6题则是相当难完成的（至今没有完成的）任务，包括但不限于形式化地表述已经存在的数学证明或者尝试一个真正的数学难题的证明。放在游戏中仅供玩家了解。
流程设计
目前讨论的结果是，考虑公理集合论、自然数、基础的证明论作为最开始的无前置的卷（官方星球）。任意完成一个即可获得全部策略。
在认知序中，由此引申开来多个卷组成的DAG，直到线性代数（或设计为高等代数）卷、数学分析卷作为阶段性的两个卷作为以上卷的汇点（后继卷的必经之路）。在这两个阶段性的卷之后，玩家可以自由探索代数、分析、几何、组合及其他领域的卷。
在归纳序中玩家遵循数学原理的序进行游玩。
游戏内的额外奖励
虽然游戏本身给予了极大的精神奖励，但是为了让这个游戏更“游戏”一点，也许需要引入额外奖励。目前思考得出的可以奖励的有：
- 不同的Q.E.D. 动画
- 多样的章节完成特效
- 完成卷获得勋章、成就、能力评价