#基石
【逻辑学】简单的形式语言及可靠性、完全性证明
选了哲学系开的Ⅲ类通识课“逻辑导论”。此文主要是做习题（之后大概也会如此），因此先快速掠过定义：…
【类型论】同伦类型论综述与 Martin-Löf 类型论
发现到时候不一定要读数院的研，考虑可以做逻辑学或者是 AI for math. 仔细阅读本书 Homotopy Type Theory: Univalent Foundations of Mathematics. 这是上学期计概老师推荐的，但当时看得太粗略了。本文包含该书的前言和第一章内容。…