课程
几何学Ⅱ期末复习笔记
下半学期的内容是基本群和复叠空间。参考尤承业《基础拓扑学讲义》及 Allen Hatcher 的 Algebraic Topology 第一章。…
高等代数Ⅱ期末复习笔记
本文用于准备高等代数Ⅱ的期末考试。这半学期的内容主要是内积空间、内积空间上的线性变换，以及双线性形式。…
数学分析Ⅱ期末复习笔记
本文用于准备数学分析Ⅱ的期末考试。这半学期的内容是函数项级数（一致收敛）、幂级数与多元函数微分学。…
一阶逻辑的元定理与边界
命题逻辑对推理的分析无法满足我们的需求，我们还需要对“所有”这样的词语分析，因而有了一阶逻辑，在满足一定条件下它是表达能力最强的逻辑系统，但也有其边界。…
命题模态逻辑与知识逻辑
发展出（命题）模态逻辑的动机来自于，命题逻辑的实质蕴涵并不总是与自然语言的“如果……那么……”完全相符，因为自然语言中还携带了因果、时间、规范、认知、反事实等信息。由于精力有限，本文涉及的内容会远少于对应的课程讲义。…
高等代数Ⅱ期中复习笔记
本文用于准备高等代数Ⅱ的期中考试。这半学期的内容是推进到准素循环分解，其动机是尽可能精细的直和分解。…
几何学Ⅱ期中复习笔记
这半学期的主要内容是古典微分几何，即嵌入 $\mathbb{E}^3$ 看的曲线论与曲面论。本文略去关于 Christoffel 记号的内容（如果之后学习黎曼几何可能涉及到更一般的）。…
数学分析Ⅱ期中复习笔记
本文用于准备数学分析Ⅱ的期中考试。这半学期的内容是定积分（Riemann 积分），广义积分（无穷积分与瑕积分）与数项级数（更多的敛散性判断与计算）。…
经典命题逻辑及其强完全性证明
这一节主要讨论的是经典命题逻辑（不同于它的均称为“非经典”），重点在于其强完全性的证明。…
形式系统概念与可靠性、完全性证明
选了哲学系开的Ⅲ类通识课“逻辑导论”。此文主要是做习题（之后大概也会如此），因此先快速掠过定义：…
几何学Ⅰ期末复习笔记
需要特别记忆的定义和结论 & 考后总结。
数学分析Ⅰ期末复习笔记
本文用于准备数学分析Ⅰ的期末考试。包含往年题、习题课需要记忆的结论与技巧 & 考后总结。…
高等代数Ⅰ期末复习笔记
本文用于准备高等代数Ⅰ的期末考试，包含往年题选做和可能有用的知识扩充 & 考后总结。…
Bird Meertens 形式与高效程序导出
主要包含使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。
这是本课程的最后一个部分，同时可能是在上半学期和下半学期前部的铺垫下真正想讲的东西。其中函数式编程的想法提供了无副作用的函数和高阶函数的例子，从而能够被我们讨论；定理证明器则允许我们验证推导的正确性。…
Agda 语言与基本的形式化证明
下半学期使用 Agda 来讲授函数式程序推理与演算，也展示了 Internal Verification 思想。…
几何学Ⅰ期中复习笔记
本文用于准备几何学Ⅰ的期中考试，包含需要特别记忆的定义和结论 & 考后总结。
几何是一个关联很多数学分支的分支，因此本文中可能涉及不那么几何的结论。…
高等代数Ⅰ期中复习笔记
本文用于准备高等代数Ⅰ的期中考试，包含可能有用的小结论记录及往年题选做 & 考后总结。…