这次我们来看看四维世界中的微观理论之元素周期律。四维原子结构一直是一件麻烦事：力的三次方反比衰减规律导致原子定态波函数不存在，科学界都公认四维世界中不可能有原子，也不可能构成物质，本文完。除了直接接受这个残酷现实，其实还是可以假设有四维世界原子，但其量子力学具体机制肯定跟三维理论完全不同。
四维元素周期表部分元素展示四维世界（十一）：元素周期表
四维元素周期表部分元素展示四维元素周期表部分元素展示四维元素周期表部分元素展示四维空间（十三）：超球谐函数
// 本文仅讨论超球面上的某偏微分方程的解，不涉及假想的四维世界物理学设定的内容，故分类在四维空间系列中。
// 提示：本文公式略多，不妨忽略细节只管欣赏各种波函数。
正120/600胞体对称性的超球谐函数，图片来自Greg Egan的网站
这次我们来看看超球面上的驻波模式——超球谐函数(Hyperspherical Harmonics)是什么样的。它们是超球面上拉普拉斯方程的解，跟可能的四维原子的波函数形状有关（计划下一篇文章再详细展开），亦可通过“超球谐光照”算法加速四维光线跟踪渲染。或许读者已经了解过球面上的球谐函数，知道关于它们的表达式是有点复杂的，本文将尽量避开这些繁复的表达式，从新的角度理解它们。
目录
类型论与机器证明简介
《同伦类型论》书的扉页
上篇文章介绍了命题逻辑、一阶逻辑再到ZFC集合论，本文来看一种新的宣称想要取代集合论在数学中地位的新东西——类型论。事实上它已经广泛运用在机器证明当中，其中最著名的就是四色定理的证明了，同时它跟程序代码很类似。把类型论稍加改造成同伦类型论，它还能比集合论更加“直接”地处理拓扑学中的许多问题。
类型论的动机
“类型”这一概念广泛被用于编程语言中，具体来说用于编译前的类型检查，比如下面这段C语言代码
1 | int i = 0; // 定义整数变量i，并将其设为0 |
编译时会报错，因为这段程序声明i是整数类型的变量，而j是字符串类型的变量，它们无法相乘，或者说，乘法运算是一个接受两个数作为输入参数，输出返回一个数的函数，这里输入的i、j的类型显然与之不匹配。从上面的例子可以看出，类型检查其实就是编译器帮助我们检查代码有没有明显的低级错误导致执行一些像把数字与字符串相乘的这种无意义的命令。虽然检查一个表达式的类型也是机械化的（可定义成形式系统），但这似乎跟数学逻辑没有一点关系，它居然能用来构建公理化体系？yugu233做过一期视频《论码农与数学家的相似性【数学地图】》非常通俗形象地解释了类型跟证明之间的联系。
四维计算机图形学：建模篇
公理化集合论简介
// 注：本文仅为作者最近学习了解集合论的大致总结，若想深入了解强烈建议找本数理逻辑的教材系统学习，维基百科也不错。
大家知道，数学有别于其它学科最重要就是严谨，比如上篇文章介绍了超越无穷的序数与基数，稍不小心就容易出错误。随着数学理论与证明过程越来越复杂，数学家急需一种能机械化规范证明的系统，使得可方便机器对其验证。在计算机发明之前就有人提出了它——形式系统。本文将从简单的形式系统开始，介绍命题逻辑、一阶逻辑，皮亚诺算数系统直到ZFC集合论这一主流数学中出镜最多的形式系统。
抱着边做边学的目的，我还慢慢搓出了一个能在网页上运行的形式系统模拟器“Deductrium”，后来又把它改造成了游戏。
Deductrium中证明“a → a”
大数数学简介
快增长层级函数可以通过不断套娃把序数转换为超级大的大数
去年CFY突然对“大数数学”与“序数”产生兴趣，还安利了个“序数增量”游戏Ordinal Markup给我，然后我就不幸成功入坑了。
极限序数
