Abstract. 本文将浅谈计算群论中的 Schreier-Sims 算法，该算法的核心思想是将群 $G$ 的信息表示为一列正规子群 $1 = G_1 \subset G_2 \subset \cdots \subset G_k = G$，通过 $G_i$ 在 $G_{i+1}$ 中的截面，回答一些重要的问题如某元素是否在群当中、某给定生成元的有限群的阶数是多少等。
本文的第二节介绍该算法使用的重要技术截面（Transversal）和 Schreier 引理，第三节介绍该算法的核心技术 BSGS，但是很遗憾我们暂时没能看懂如何求解一组 BSGS，只能给出一类大多数应用问题的简单快速的下替算法（参见第 3.3 节）。
Abstract. 软件科学基础的复习笔记。
课程网站是 https://xiongyingfei.github.io/SF/2024/，参考资料是 Software Fundations 的 Vol. 1 和 Vol. 2。
Abstract. AI 基础复习笔记。背书。
里面有一些不知道有什么道理的批话，均用斜体表出。
Abstract. 一些多元微积分的内容，严格来说和 Tensor 关系不大，和 Vector 关系比较大。就当是学物理了。
之前看过一次这一章，实际上没怎么看懂，写的东西很不得要领，于是删了重写。
Abstract. 是谁没有 Mac 也没装 Linux 就来选 Software Fundations 啊🤣👉
原来是我🤡🤡🤡
讲一下今晚上配置 coq 环境的流程以及踩的所有坑。其实可能有的地方记不太清楚了。
配置时间和环境：2024. 2. 22，本地环境为 Windows 11 22621.3155，vscode 1.86.2，wsl 发行版为 Ubuntu 22.04，但是感觉未必需要对着配置。
Keywords. 环境配置, wsl, WSL_E_CONSOLE, Coq, VsCoq, opam。
Abstract. 最不想学 FP 的一集《三句话让我写了一晚上形式化验证》。
本文讲如何在 Agda 中定义《数理逻辑与集合论 (1) 命题逻辑》中提到的演绎系统，并形式化验证了文中的几个定理。
好像现在我们的姿势还不太正确，我们确实找到了一种方法来验证一个证明对不对，但是对自己证明定理没有一点帮助（甚至有负贡献）。