通过Lean4语言入门学习数学证明并搭建魔方群的若干定理，3D模型使用等课程教学目标:学会Lean4数学建模魔方群，学会魔方基本定理的证明，学会使用3D魔方建模的htm嵌入显示，掌握后续魔方定理探索的能力。 1.确定项目任务，从发明者角度引入知识探索。根据学生程度制定不同的 项目任务，低程度的只需要搭建起模型，中程度的进行定理的证明，高程度 的进行更多定理的探索与推广，证明。2.实施项目任务计划。应不同程度学生的学习进度，开启服务全部学生的 Zulip，一个Lean4官方社区认证的讨论组，每一个学生的提问都总结成#mwe(最小问题)，经过老师或学生之间的回答和讨论一个个得到解决，然后迭代问 题列表服务后续学生加速学习。3.效果评价阶段。每个学生都会有各程度的小考核和小问题，根据Lean4 的严格机器验证程序来对学生完成的问题进行考量，可以准确的找出未完成 证明的问题，并且使用ITP(交互式证明工具)进行每一步的证明检验。 各章节教学内容: 0.前置知识:数学形式化证明语言LEAN4知识入门。 1.魔方建模:魔方知识入门。 2.群论知识入门，魔方超群搭建与证明，魔方群搭建与证明。4个描述项决定一个魔方群元素。 3.引入5个魔方极简基本公式，自定义“一阶交换子公式”，自定义“躲避法公式”，理解别人的公式。 4.魔方第二基本定理充分必要条件的文字证明+形式化证明。 所有证明的详细逐行讲解。 5.React3D构建魔方3D模型的介绍。如何理解别人的魔方公式6.52步算法“TW算法”的文字证明。还有形式化命题的构建。7.未来的任务:20步算法Kociemba的存在性证明。2个魔方群元素等价的充分必要条件。寻找简化魔方操作的算法，也就是寻找某个魔方群元素等价的最小复合操作的元素。课程实施计划: 1.为了教学任务能够如计划进行，首先我们专门设计了入门项目环境的多 个 入口，包括在线gitpod虚拟机容器使用和本地程序安装，在线程序模拟 使用等 多个。2.组建学生讨论组，zulip讨论组提供给学生们提问和解决问题的专属地方,提问和解决的状态，引用问题和自由讨论的学习环境，可以加速学生迭代学 习和交流的进程。课程讲解与管理流程，通过视频学习和群聊的方式获取最新的学习动态， 摒弃语言学习的只专注语言本身的旧俗，让学生更多精力专注于数学建模与 知识应用和证明的过程，ITP(交互式证明工具)进一步提高了学生的学习兴 趣与学习动力。