Lean4Game 开发教程 | 数学形式化

news2024/11/14 13:59:09

引言

Lean 是一门用于形式化证明的编程语言,它允许严格证明数学定理和验证软件代码的正确性。

本篇介绍 Lean 游戏的编写和发布方式。这类游戏不仅利于对 Lean 本身的学习,对学科知识的理解,还能推动数学圈内人对 Lean 的接触学习。

Lean4 的安装及环境管理,可以参考上一篇:Lean 4 安装教程及环境管理

相关项目与资源

教程涉及的项目和资源链接:

  • lean4game:LEAN 社区驱动的项目,用于开发 Lean4 游戏(GitHub 仓库)。
  • GameSkeleton:Lean4 游戏的模板代码(GitHub 仓库)。
  • NNG4:自然数游戏,从皮亚诺公理开始,构建自然数的基本运算和性质(GitHub 仓库)。

社区官网目前贴了自然数和集合论等游戏,也欢迎根据自己的学科知识,贡献更多的游戏~

发布游戏

我们通过一个简单的示例介绍游戏的发布过程。

下载游戏模板

首先,下载 GameSkeleton 模板仓库:

git clone https://github.com/hhu-adam/GameSkeleton.git

文件结构如下:

├── Game
│   ├── Levels
│   │   ├── DemoWorld
│   │   │   └── L01_HelloWorld.lean
│   │   └── DemoWorld.lean
│   └── Metadata.lean
├── Game.lean
├── LICENSE
├── README.md
├── lake-manifest.json
├── lakefile.lean
└── lean-toolchain

这是一个标准的 Lean 包结构,其中 lean-toolchainlakefile.leanlake-manifest.json 是 Lean 包的基本文件。Game 文件夹包含游戏内容,而 Game.lean 是游戏的入口文件。

更新依赖并构建项目:

lake update -R
lake build

类似地,也可以下载其他游戏模板,例如 NNG4:

# cd .. # 回到同一级目录
git clone https://github.com/leanprover-community/NNG4.git
cd NNG4
lake update -R
lake build

下载 Lean4Game

Lean4Game 是游戏的前后端框架,用于创建游戏的主页面。

首先,安装 Node.js 和 npm,然后下载 Lean4Game,并将其放在游戏的同级目录

# 安装 nvm
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.3/install.sh | bash
# 安装 nodejs
nvm install node
nvm use node
# 下载 Lean4Game
git clone https://github.com/leanprover-community/lean4game.git
cd lean4game
# 安装依赖
npm install --force

推荐使用的 Node 版本是 22.2.0。执行 npm start 启动游戏,或者指定服务端口:

export PORT=8080
export CLIENT_PORT=3000
npm start

这里 PORT 为运行 Lean 代码的后端端口,默认是 8080;CLIENT_PORT 为前端访问端口,默认是 3000。

如果看到以下页面,就表示访问成功:

20240623121710

此外,可以在右上角的偏好设置中选择语言:

20240623164430

Nginx 配置

如果一切顺利,访问 http://localhost:3000/#/g/local/GameSkeleton 会看到 “Hello World” 的界面:

20240623130158

假设服务启动在 3000 端口,可以将域名 game.leanprover.cn 配置为游戏主页面,参考配置如下:

server {
    listen 443 ssl;
    ssl_certificate /etc/letsencrypt/live/game.leanprover.cn/fullchain.pem; 
    ssl_certificate_key /etc/letsencrypt/live/game.leanprover.cn/privkey.pem; 
    server_name game.leanprover.cn;
    location / {
        proxy_pass http://localhost:3000;
        proxy_set_header Upgrade $http_upgrade;
        proxy_set_header Connection "Upgrade";
        proxy_set_header Host $host;
        proxy_read_timeout 86400;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
        proxy_ssl_server_name on;
        proxy_http_version 1.1;
        chunked_transfer_encoding off;
        proxy_buffering off;
        proxy_cache off;
        proxy_set_header X-Forwarded-Proto $scheme;
        client_max_body_size 0;
    }
}

为简化输入,可以为游戏单独配置一个子域名进行跳转,例如 nng4.leanprover.cn

server {
    listen 443 ssl; 
    ssl_certificate /etc/letsencrypt/live/nng4.leanprover.cn/fullchain.pem;
    ssl_certificate_key /etc/letsencrypt/live/nng4.leanprover.cn/privkey.pem;
    server_name nng4.leanprover.cn;
    return 301 https://game.leanprover.cn/#/g/local/NNG4;
}

这样只需访问 nng4.leanprover.cn,而不需要输入后面的一长串 URI。

游戏修改指南

本节以 NNG4 为例,介绍游戏文件结构和如何添加游戏内容。

游戏入口 Game.lean

文件 Game.lean 是整个游戏的主干,负责整合所有内容。以下是示例代码:

import GameServer.Commands

-- 导入所有世界
import Game.Levels.Tutorial

Title "My Game"

Introduction "
Hi, nice you're here! Click on a world to start.
"

Info "
This game has been developed by me.
"

-- Dependency World₁ → World₂ -- 由于使用了 `≠`
MakeGame

代码解析:

  1. import:导入游戏服务器命令。其中 GameServer 是从 lean4game 引入的,不是来自当前的模板仓库。
  2. Title "My Game":设置游戏的标题。
  3. Introduction:在世界选择界面旁显示的介绍文本。
  4. Info:在游戏菜单中显示的信息,介绍游戏的背景和开发者信息等。
  5. Dependency:一个可选命令,用于设置世界之间的依赖关系。例如,若一个世界介绍了 符号,而在另一个世界中用户需要已知此符号,则可使用此命令。
  6. MakeGame:构建游戏的命令。如果存在需要修复的问题,将以警告或错误的形式显示(在 VSCode 中为橙色/红色波浪线)。

可对照下图:

20240623142725

创建关卡

下面是一个最简关卡文件示例:

import GameServer.Commands

World "MyWorld"
Level 1
Title "Hello World"

Introduction "
A message shown at the beginning of the level. Use it to explain any new concepts.
"

/-- The exercise statement in natural language using latex: $\iff$. -/
Statement (n : Nat) : 0 + n = n := by
  sorry

Conclusion "
The message shown when the level is completed
"

操作步骤:

  1. 创建文件夹 Game/Levels/MyWorld
  2. 创建文件 Game/Levels/MyWorld/L01_hello.lean
  3. 将上述代码复制到你的第一个关卡文件中。
创建世界

接下来,我们创建一个世界。需要创建一个名为 MyWorld.lean 的文件,并将所有关卡文件导入到该世界中:

import Game.Levels.MyWorld.L01_hello

World "MyWorld"
Title "My First World"

Introduction "
This introduction text is shown when one first enters a world.
"

操作步骤:

  1. 创建文件 Game/Levels/MyWorld.lean
  2. 使用上面的模板,确保导入了该世界的所有关卡。
  3. Game.lean 中导入该世界:import Game.Levels.MyWorld

至此,我们已成功创建一个包含一个关卡的世界并将其加入到游戏中 🎉。

Game.lean 中的 MakeGame 命令会指出需要修复的任何问题。例如,如果显示:

makegame

这意味着世界 MyWorld 使用了 sorry 策略,但此策略尚未在任何地方被引入。

每次添加或修改游戏内容后,都需要重新构建更新:

# cd NNG4 # 进入游戏目录
lake build

高级交互特性

接下来我们将粗略介绍游戏中的高级交互功能。这部分功能十分丰富,目前只进行初步说明。后续添加小游戏的过程,再进一步拓展和补充。

定理和策略的管理

玩家在游戏中拥有一个逐步解锁的定理和策略清单。在关卡设计中,通过以下命令在 Statement 下方解锁或引入新的定理和策略:

NewTactic induction simp -- 解锁 `induction` 和 `simp`
NewTheorem Nat.zero_mul
NewDefinition Pow

重要提示:所有命令中的名称都需要使用全限定名。例如,应使用 NewTheorem Nat.zero_mul 而非 NewTheorem zero_mul

文档条目

如果发现定理文档缺失,系统会显示警告。可以通过添加文档条目解决这一问题:

/--
some description
-/
TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"

/--
some description
-/
TacticDoc simp

/--
some description
-/
DefinitionDoc Pow as "^"

创建一个文件 Game/Doc/MyTheorems.lean,在其中添加文档并将其导入项目中。

如果未提供任何文档内容,游戏将尝试寻找并展示该条目的文档字符串。

清单管理

玩家可以通过以下命令在关卡中禁用或只启用特定的已解锁条目:

DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem

这些命令的语法与前边相同。前两个命令用于禁用该关卡的特定条目,后两个命令用于只启用指定的条目。

定理标签

通过 TheoremTab "Mul" 命令为定理分组,并指定在关卡中默认打开的标签。

隐藏策略

使用 NewHiddenTactic 命令可以添加允许策略而不在玩家清单中显示。例如:

NewTactic rw
NewHiddenTactic rewrite nth_rewrite rwa

在此例中,只有 rw 会在清单中显示。

关卡设计

通过一个示例来查看关卡的代码:

/-- 我们定义一个从 ℕ 到 ℕ 的函数。 -/
Statement
    : ℕ → ℕ := by
  Hint "为了解决这个目标,
  你需要构想一个从 `ℕ`
  到 `ℕ` 的函数。开始使用

  `intro n`"
  intro n
  Hint "我们的任务现在是构造一个自然数,这个数可以依赖于 ${n}。我们可以使用 `exact` 并写出我们想要定义的函数的公式。例如
  我们在文件顶部导入了加法和乘法,
  所以

  `exact 3 * {n} + 2`

  将完成目标,最终定义函数 $f({n})=3{n}+2$."
  exact 3 * n + 2

Statement 用于定义练习,其用法类似于 exampletheorem,但必须使用策略证明,即 := by 是固定的语法部分。

Statement 可以接练习的命名,比如:Statement my_first_exercise (n : Nat) …。命名后它会被添加到清单中,并在后续关卡中可用。

此外,Statement 前的注释将作为练习的描述显示在游戏中,且支持 Latex。

证明

证明必须是策略证明,即 := by 是固定的语法部分。

以下是一些有助于结构化证明的策略:

  • Hint:可以使用 Hint "text" 在游戏的目标状态匹配时显示文本。更多关于提示的选项,请参见相关文档。
  • Branch:可以在证明中添加 Branch,执行替代策略序列,帮助在不同位置设置 HintBranch 不会影响主证明且不需完成任何目标。
  • Template/Hole:用于提供示例证明模板。Template 中的内容将被复制到编辑器中,所有 Hole 将被替换为 sorry。注意,拥有 Template 将强制用户在该关卡使用编辑器模式。

提示

提示是游戏开发中可能是最重要的部分。提示将在玩家的当前目标与示例证明中的目标匹配时显示。可以使用 Branch 在死胡同或替代证明路径中设置提示。

添加图片

可以在游戏的任何层级(游戏/世界/关卡)添加图片,这些图像将显示在游戏中。

文件需放置在 images/ 中,并通过在创建的文件中添加如 Image "images/path/to/myWorldImage.png" 的命令来引用。

注意事项

设计新游戏时应考虑的其他事项:

  • 在字符串内部需要转义反斜杠,但在文档注释的字符串内部则不需要,因此你会写 Introduction "some latex here: $\\iff$."/-- some latex here: $\iff$. -/ Statement ...
  • 拥有超过 16 个关卡的世界将以螺旋形向外显示,最好保持在这个范围以下。超过 22 个关卡时,螺旋形开始变得难以控制。

游戏翻译

通过使用 lean-i18n 和 i18next,可以为游戏添加多语言支持。TODO Ref: https://github.com/leanprover-community/lean4game/blob/main/doc/translate.md


以上,一些内容细节待补充完善,欢迎交流~

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.coloradmin.cn/o/1872639.html

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈,一经查实,立即删除!

相关文章

你不知道的物联网产品有那么多

目录 1. 智能农业设备 ​编辑1.1 土壤感应器 1.2 自动喷灌系统 2. 智能医疗设备 ​编辑2.1 可穿戴健康监测设备 2.2 智能药盒 3. 智能城市基础设施 ​编辑3.1 智能垃圾桶 3.2 智能路灯 4. 智能物流与供应链 ​编辑4.1 货物跟踪设备 4.2 智能仓储系统 5. 智能网关 …

linux server下人脸检测与识别服务程序的系统架构设计

一、绪论 1.1 定义 1.2 研究背景及意义 1.3 相关技术综述 二、人脸检测与识别技术概述 2.1 人脸检测原理与算法 2.2 人脸识别技术及方法 2.3 人脸识别过程简介 三、人脸检测与识别服务程序的系统架构 3.1 系统架构设计 3.2 技术实现流程 四、后续设计及经验瞎谈 4.…

【Mac】Listen 1 for Mac(最强的音乐搜索工具)软件介绍

软件介绍 Listen 1 for Mac 是一款非常方便的音乐播放软件,主要功能是集成多个音乐平台,让用户可以方便地搜索、播放和管理音乐。它是一个用 Python 语言开发的免费开源综合音乐搜索工具项目,最大的亮点在于可以搜索和播放来自网易云音乐&am…

全国公共汽车、出租车拥有情况及客运量、货运量数据

基本信息. 数据名称: 全国公共汽车、出租车拥有情况及客运量、货运量数据 数据格式: Shp、Excel 数据时间: 2020-2022年 数据几何类型: 面 数据坐标系: WGS84 数据来源:中国城市统计年鉴 数据可视化. 2022年全年公共汽车客运总量数据示意图 2022年公路客…

Apifox 更新|定时任务、内网自部署服务器运行接口定时导入、数据库 SSH 隧道连接

Apifox 新版本上线啦! 看看本次版本更新主要涵盖的重点内容,有没有你所关注的功能特性: 自动化测试支持设置「定时任务」支持内网自部署服务器运行「定时导入」数据库均支持通过 SSH 隧道连接自动化测试数据库操作优化 1、自动化测试支持设…

计算机语言vs指令vs中央处理器cpu

计算机中如何表示数据 在计算机中,所有数据和指令都是用二进制表示的,即0和1。这些0和1实际上是电压信号的高低电平,0通常表示低电平(如0伏特),1表示高电平(如5伏特)。 指令系统&a…

基本的 Spring Boot 配置步骤和常见的配置项【创建,配置,日志,数据库,安全,MVC】

基本的 Spring Boot 配置步骤和常见的配置项【创建,配置,日志,数据库,安全,MVC】 学习总结 1、掌握 JAVA入门到进阶知识(持续写作中……) 2、学会Oracle数据库入门到入土用法(创作中……) 3、…

UE5基本操作(二)

文章目录 前言相机的移动速度修改默认地图使用初学者内容包文件夹结构 总结 前言 在我们的上一篇文章中,我们已经介绍了一些Unreal Engine 5(UE5)的基本操作。UE5是一款强大的游戏开发引擎,它提供了许多工具和功能,使…

Elasticsearch 聚合查询

Hi~!这里是奋斗的小羊,很荣幸您能阅读我的文章,诚请评论指点,欢迎欢迎 ~~ 💥💥个人主页:奋斗的小羊 💥💥所属专栏:C语言 🚀本系列文章为个人学习…

SpringMVC处理器映射器HandlerMapping详解

目录 一、前言 二、initHandlerMappings 三、处理器映射器架构 策略接口 请求链 模版类 四、RequestMappingHandlerMapping的初始化 HandlerMethod映射器模版类的初始化 AbstractHandlerMethodMapping.MappingRegistry:内部类注册中心 五、Reques…

AST反混淆|某练习平台混淆代码彻底还原及逆向请求

关注它,不迷路。 本文章中所有内容仅供学习交流,不可用于任何商业用途和非法用途,否则后果自负,如有侵权,请联系作者立即删除! 一.目标地址 https://match.yuanrenxue.cn/match/2 二.代码还原 初次请…

MongoDB:JSON and BSON

目录 什么是 JSON MongoDB-JSON连接 什么是 BSON MongoDB 使用 BSON 还是 JSON JSON 与 BSON 架构灵活性和数据治理 JSON 和 BSON 是近亲,正如它们几乎相同的名称所暗示的那样JSON(即 JavaScript 对象表示法)是网络上广泛流行的数据交换…

CVPR上新 | 从新视角合成、视频编解码器、人体姿态估计,到文本布局分析,微软亚洲研究院精选论文

编者按:欢迎阅读“科研上新”栏目!“科研上新”汇聚了微软亚洲研究院最新的创新成果与科研动态。在这里,你可以快速浏览研究院的亮点资讯,保持对前沿领域的敏锐嗅觉,同时也能找到先进实用的开源工具。 本周&#xff0…

2024年湖北省安全员-C证证考试题库及湖北省安全员-C证试题解析

题库来源:安全生产模拟考试一点通公众号小程序 2024年湖北省安全员-C证证考试题库及湖北省安全员-C证试题解析是安全生产模拟考试一点通结合(安监局)特种作业人员操作证考试大纲和(质检局)特种设备作业人员上岗证考试…

uni-app通过配置package.json实现环境变量、自定义条件编译

文章目录 前言官方提示使用方法微信小程序配置如下自定义条件编译使用方法 前言 uni-app 官方概括 官方文档 在开发web时,有时需要一套代码编译发布到不同的站点,比如主站和微信h5站。(注意不是一套代码内部自适应不同浏览器,是真…

CentOS 生命周期结束指南

2019 年 9 月,Red Hat 宣布打算废止 CentOS,并将其替换为 CentOS Stream。 CentOS 7 和 8 是 CentOS Linux 的最终版本。CentOS 7 和 8 的生命周期结束日期为: CentOS 8 - 2021 年 12 月 31 日 CentOS 7 - 2024 年 6 月 30 日 相关内容推荐 点…

MySQL数据库存储引擎

MySQL数据库存储引擎 存储引擎概念 存储引擎也称为表类型 通过不同的技术比如说,存储机制,索引技巧,锁定水平等等,来提供不同的功能。 查看MySQL支持的存储引擎 show engines\G; 常用引擎比较 对事务有需求 innodb …

MySQL丢失更新问题的出现和解决

MySQL丢失更新问题的出现和解决 丢失更新问题(Lost Update)指的是两个或多个事务在读同一数据并基于此数据进行更新操作时,某些更新操作被覆盖或丢失。例如,事务A和事务B都读取了某个数据,然后事务A更新了该数据&…

谷歌Gemma 2:开源模型的新里程碑

引言: 在人工智能领域,谷歌一直是创新的先行者。最近,谷歌DeepMind团队在I/O Connect大会上发布了Gemma 2,这是其开源模型系列的最新力作,标志着AI技术的又一大步。 Gemma 2的前身,Gemma,已经因…

0-30 VDC 稳压电源,电流控制 0.002-3 A

怎么运行的 首先,有一个次级绕组额定值为 24 V/3 A 的降压电源变压器,连接在电路输入点的引脚 1 和 2 上。(电源输出的质量将直接影响与变压器的质量成正比)。变压器次级绕组的交流电压经四个二极管D1-D4组成的电桥整流。桥输出端…