Brunerie 数

Guillaume Brunerie 使用同伦类型论证明了以下命题 [Brunerie 2016]:

命题 0.1. 存在整数 $n$ 使得 ${\pi }_4(S^3)=\mathbb{Z}/n\mathbb{Z}$.

这个数被称为 $\text{Brunerie 数}$. 经典同伦论表明 $n$ 必须等于 $\pm 2$, Brunerie 也在同伦类型论中证明了这一点. 需要强调的是, Brunerie 数的定义是构造主义的. 因此, 在具有计算意义的同伦类型论中, 计算机可以自动计算出该数的值.

Brunerie 构造了一组函数, 将其复合可以得到 Brunerie 数. 他的构造深度依赖于泛等公理的计算性质, 因此立方类型论由于 Swan 问题而对计算该值有很大劣势.

$$\mathbb{Z}\Omega (S^1){\Omega }^2(S^2){\Omega }^3(S^3){\Omega }^3(S^1\ast S^1){\Omega }^3(S^2){\Omega }^3(S^1\ast S^1){\Omega }^3(S^3){\Omega }^2\Vert S^2{\Vert }_2\Omega \Vert \Omega (S^2){\Vert }_1\Vert {\Omega }^2(S^2){\Vert }_0\Omega (S^1)\mathbb{Z}{\Omega }^3\alpha$$

Axel Ljungström 对该表达式进行简化, 避免使用同调论. 这个版本的 Brunerie 数最终被计算出来, 但结果变成了 $n=-2$.

Anders Mörtberg 发现, 对于一串函数 $\mathbb{Z}\simeq H^2(\mathbb{C}{P}^2)\to H^4(\mathbb{C}{P}^2)\simeq \mathbb{Z}$, 若输入 $1$, 应当返回 $\pm 1$, 但这个函数也没能计算出来.

目前只有 András Kovács 仍尝试在立方类型论中计算最初的 Brunerie 数, 其他实验均因为表达式体积过大而以失败告终. 目前最狠的一次尝试是 Favonia 使用了一台 1TB 内存的电脑, 最终该程序在 90 小时后内存溢出.

1影响

Guillaume Brunerie 为了构造这个数字, 大力发展了综合同伦论, 将大量的经典结论翻译到了同伦类型论, 并给出只使用类型论的证明.

为了编译和运行这个数字对应的程序, 也启发了很多立方类型论中的研究, 例如泛等公理相关的内存优化等.

2参考文献

•	Guillaume Brunerie (2016). “On the homotopy groups of spheres in homotopy type theory”. arXiv: 1606.05916. (doi) (web)