知识
几何学Ⅱ期中复习笔记
这半学期的主要内容是古典微分几何，即嵌入 $\mathbb{E}^3$ 看的曲线论与曲面论。本文略去关于 Christoffel 记号的内容，这见于之后黎曼几何。…
数学分析Ⅱ期中复习笔记
本文用于准备数学分析Ⅱ的期中考试。这半学期的内容是定积分（Riemann 积分），广义积分（无穷积分与瑕积分）与数项级数（更多的敛散性判断与计算）。…
经典命题逻辑及其强完全性证明
这一节主要讨论的是经典命题逻辑（不同于它的均称为“非经典”），重点在于其强完全性的证明。…
形式系统概念与可靠性、完全性证明
选了哲学系开的Ⅲ类通识课“逻辑导论”。此文主要是做习题（之后大概也会如此），因此先快速掠过定义：…
类型论导引与 Martin-Löf 类型论
发现到时候不一定要读数院的研，考虑可以做逻辑学或者是 AI for math. 仔细阅读本书 Homotopy Type Theory: Univalent Foundations of Mathematics. 这是上学期计概老师推荐的，但当时看得太粗略了。本文包含该书第一章内容。…
《初识量子力学》笔记（上）
参考的是《初识量子力学》前三章，这是一个理顺量子力学理论的尝试。读者可先阅读《初识经典力学》笔记。…
基于有限域上数论的密码系统
主要参考的是 An Introduction to Mathematical Cryptography 第二章离散对数、第三章整数分解及第四章数字签名。…
几何学Ⅰ期末复习笔记
需要特别记忆的定义和结论 & 考后总结。
数学分析Ⅰ期末复习笔记
本文用于准备数学分析Ⅰ的期末考试。包含往年题、习题课需要记忆的结论与技巧 & 考后总结。…
Banach–Tarski 分球定理的证明细节
Banach–Tarski 分球佯谬说的是，可以把 $\R^3$ 中的单位球分成有限个（可以做到 5 个）点集的无交并，仅用旋转与平移重新拼合，得到两个完整的单位球。这从纯集合论角度是合理的，但整个结论是反直觉的。…
高等代数Ⅰ期末复习笔记
本文用于准备高等代数Ⅰ的期末考试，包含往年题选做和可能有用的知识扩充 & 考后总结。…
Bird Meertens 形式与高效程序导出
主要包含使用 Bird Meertens Formalism 导出高效程序与进行自动并行化。
这是本课程的最后一个部分，同时可能是在上半学期和下半学期前部的铺垫下真正想讲的东西。其中函数式编程的想法提供了无副作用的函数和高阶函数的例子，从而能够被我们讨论；定理证明器则允许我们验证推导的正确性。…
Hash 与基于哈希的 table 实现
阅读一下 Rust 标准库的 Hash 与 RawTable 相关代码。本文参考的 Rust 版本是 1.90.0-nightly…
一些泛性质使用的习题选做
选做 Saunders Mac Lane 的书 Categories for the Working Mathmatician 第二版中一些不废话的习题，包含 Ⅱ. Constructions on Categories 及 Ⅲ. Universals and Limits 的 1. Universal Arrows 节。…
单复变 Weierstrass 级数理论
一般认为 Cauchy 积分理论、Weierstrass 级数理论和共形映射理论是单复变函数理论中的三个最重要的组成部分。
本章内容为 Laurent 级数与留数。…
量子信息的基本原理与基本结论
量子信息的一些系统学习。从量子状态定义到量子密集编码、量子隐形传态、纠缠的量化。
光滑流形（一）：切空间与微分形式
我们来看了解 $\partial/\partial x$，$\mathrm{d}/\mathrm{d}x$ 及更复杂的记号在一般的流形上的推广是什么。…
单复变 Cauchy 积分理论
复变会告诉你：性质好的函数性质有多好。…
Agda 语言与基本的形式化证明
下半学期使用 Agda 来讲授函数式程序推理与演算，也展示了 Internal Verification 思想。…
几何学Ⅰ期中复习笔记
本文用于准备几何学Ⅰ的期中考试，包含需要特别记忆的定义和结论 & 考后总结。
几何是一个关联很多数学分支的分支，因此本文中可能涉及不那么几何的结论。…