P60 五维空间中的十六条直线：网格最优值已证明

0. 记号

一个答案是 16 个非零向量 v₁, …, v₁₆ ∈ ℝ⁵，每个坐标是 [−1, 1] 内至多九位小数的十进制数。向量代表它张成的直线，正负和缩放都不改变答案。记

q = μ² = max over i < j of (vᵢ·vⱼ)² / ((vᵢ·vᵢ)(vⱼ·vⱼ)), K = ceil(10¹⁸ q).

K 是本站记录的整数分数，越小越好；页面显示 √(K/10¹⁸) 向上取整到九位小数。q 是有理数，验证器用交叉相乘精确比较，不做归一化也不开方。

记 uᵢ = vᵢ/|vᵢ| 为单位代表，sᵢ = vᵢ·vᵢ。两条直线 i、j 称为等号对，如果 (uᵢ·uⱼ)² = 1/5。第 2–6 节只用到 vᵢ 的坐标是有理数，所以 (b) 对任意分母的有理坐标都成立，不只是 10⁹。

1. 下界与取等构型

对每条直线令 Qᵢ = uᵢuᵢᵀ − I₅/5。Qᵢ 是迹为零的 5 阶实对称矩阵，这个空间的维数是 15 − 1 = 14。以 Frobenius 内积 ⟨A, B⟩ = tr(AB) 取它们的 Gram 矩阵 H：

Hᵢᵢ = 4/5, Hᵢⱼ = tr(QᵢQⱼ) = (uᵢ·uⱼ)² − 1/5 (i ≠ j).

H 是 16 阶半正定矩阵，秩至多 14，所以 dim ker H ≥ 2。另外 cᵀHc = ‖Σ cᵢQᵢ‖²，因此 Hc = 0 当且仅当 Σ cᵢQᵢ = 0。

引理 1.1（Perron 型核引理）。 设 H 半正定、非对角元都 ≤ 0，并且以 Hᵢⱼ < 0 为边的图连通。若 H 奇异，则 ker H 是一维的，并由一个各坐标严格为正的向量张成。

证明：取非零 z ∈ ker H，记 |z| 为逐坐标取绝对值。因为非对角元非正，|z|ᵀH|z| ≤ zᵀHz = 0；半正定性给出 |z|ᵀH|z| = 0，从而 H|z| = 0。若非负核向量 y 的某个坐标 yᵢ = 0，则第 i 个方程 Σⱼ Hᵢⱼyⱼ = 0 只含非正项，迫使 i 的每个负边邻居 yⱼ = 0；沿连通图传开，y = 0。所以 |z| 的每个坐标都严格为正。取一个正核向量 x，对任意核向量 z 令 c = maxᵢ zᵢ/xᵢ，则 cx − z 是非负核向量且有零坐标，只能为零，于是 z = cx。

命题 1.2（Rankin 界）。 任意 16 条直线都有 q ≥ 1/5。若 q < 1/5，H 的全部非对角元严格为负，图是完全图，由引理 1.1 核至多一维，与 dim ker H ≥ 2 矛盾。这正是 Rankin 的正交多面体界：N > d(d + 1)/2 条直线时 μ² ≥ 1/d，这里 d = 5、N = 16 > 15。

取等构型（6 + 10）。 把 ℝ⁵ 看成 ℝ⁶ 中的超平面 x₁ + … + x₆ = 0，j = (1, …, 1)。六条单纯形直线 uᵢ = √(6/5)(eᵢ − j/6) 是单位向量，uᵢ·uⱼ = −1/5。对 {1, …, 6} 的每个三元子集 S，令 v(S) 在 S 上为 +1/√6、在补集上为 −1/√6；S 与补集给出同一条直线，共 10 条。v(S) 坐标和为 0，所以 uᵢ·v(S) = ±1/√5；当 T ≠ S 且 T 不是 S 的补集时，v(S)·v(T) = ±1/3。全部平方重合度属于 {1/25, 1/9, 1/5}，最大为 1/5。

另一个取等构型（7 + 9）。 取单位向量 e₀，以及与 e₀ 正交、彼此正交的两个平面里的正三角单位向量组 t₁, t₂, t₃ 与 s₁, s₂, s₃（每组两两内积 −1/2）。七条直线 e₀、−e₀/3 + (2√2/3)tᵢ、−e₀/3 + (2√2/3)sⱼ，九条直线 (e₀ + √2(tᵢ + sⱼ))/√5。直接计算：跨组平方重合度全为 1/5；七条之间为 1/9 或 1/81；九条之间为 4/25 或 1/25。因此 (a) 成立。16 条线的已知最优构型收录在 Henry Cohn 的 Grassmannian 打包档案中。

2. 等号结构：块、紧框架与奇环

从这里到第 6 节末，反设 v₁, …, v₁₆ 有理且 q ≤ 1/5，最终导出矛盾。由命题 1.2，q = 1/5，所以 H 的非对角元都 ≤ 0，引理 1.1 适用于以 Hᵢⱼ < 0 为边的图的每个连通分支，称之为块。

引理 2.1（等号边没有奇环）。 若 i、j 是等号对，则 sᵢsⱼ = 5(vᵢ·vⱼ)²，且 vᵢ·vⱼ ≠ 0。沿长度为奇数 k 的环把这些等式相乘，左边每个 sᵢ 出现两次，是一个非零有理数的平方；右边是 5ᵏ 乘一个非零有理平方。于是 5 是有理数的平方，矛盾。特别地，没有三条直线两两成等号对。

引理 2.2（恰好两个块）。 不同块之间 Hᵢⱼ = 0，即跨块的每一对都是等号对。三个块各取一条线就是等号三角形，由引理 2.1 块数至多为 2。H 按块分成分块对角阵，ker H 是各块核的直和；由引理 1.1 每块至多贡献一维（单条线的块是 4/5，非奇异）。dim ker H ≥ 2，所以恰有两个块，两个都奇异，各有一个严格正的核向量，且 rank H = 14。

引理 2.3（正权紧框架）。 设 c > 0 是某块的核向量，则 Σ cᵢQᵢ = 0，即 Σ cᵢuᵢuᵢᵀ = (Σ cᵢ/5)I₅。令 wᵢ = 5cᵢ/Σ cⱼ，得

Σ wᵢ uᵢuᵢᵀ = I₅, wᵢ > 0, Σ wᵢ = 5 (sum over one block).

（Σ wᵢ = 5 来自取迹。）所以每块的直线张成 ℝ⁵，至少有 5 条。每块内部没有等号对：块内的等号对与另一块任一条线构成等号三角形。

总结：两块 A、B，|A| + |B| = 16，每块都是正权紧框架，跨块每对满足 |a·b| = 1/√5（单位代表），块内每对满足 (a·a′)² < 1/5。

3. 块的大小：排除 5 + 11 与 6 + 10

块的大小只可能是 (5, 11)、(6, 10)、(7, 9)、(8, 8)。本节排除前两种，其中 6 + 10 化为正则单纯形，由第 6 节的算术障碍排除。

3.1 五条线的块

五条线的正权紧框架：以 √wᵢuᵢ 为列的 5 × 5 矩阵 W 满足 WWᵀ = I，因此 WᵀW = I，即 √(wᵢwⱼ) uᵢ·uⱼ = δᵢⱼ：五条线是正交基，权重全为 1。另一块的每条线与五个基向量的内积绝对值都是 1/√5，所以在这组基下坐标为 (±1, …, ±1)/√5。两条这样的线内积是五个 ±1 之和除以 5，即奇数除以 5，绝对值属于 {1/5, 3/5, 1}；相干界 1/√5 只容许 1/5。

设有 N 条这样的线，单位 Gram 矩阵 G 的秩 ≤ 5、迹为 N，非对角元平方为 1/25。由 Cauchy–Schwarz 作用于 G 的特征值，(tr G)² ≤ 5 tr(G²)：

N² ≤ 5(N + N(N − 1)/25) ⟹ 4N ≤ 24 ⟹ N ≤ 6.

（穷举表明实际最大值是 5。）另一块需要 11 条线，矛盾。

3.2 六条线的块

设六条线满足 Σ wᵢuᵢuᵢᵀ = I₅。以 √wᵢuᵢ 为列的 5 × 6 矩阵 W 行正交单位，所以 WᵀW = I₆ − zzᵀ，z 是 W 的行空间的单位法向量。比较对角元与 Wz = 0：

wᵢ = 1 − zᵢ² > 0, Σ cᵢuᵢ = 0 with cᵢ = zᵢ√(1 − zᵢ²).

翻转 uᵢ 的方向（同时翻转 zᵢ 的符号）可设 zᵢ ≥ 0，于是 cᵢ ≥ 0，且 cᵢ = 0 当且仅当 zᵢ = 0。另一块的每条单位向量 v 给出符号 εᵢ = √5 uᵢ·v ∈ {±1}，并且 Σ cᵢεᵢ = √5 (Σ cᵢuᵢ)·v = 0，称 ε 为平衡的。六条 uᵢ 张成 ℝ⁵，所以 ε 唯一确定 v；−ε 对应同一条直线。十条线因此需要至少 20 个平衡符号向量。记 m 为正的 cᵢ 的个数。

m = 6. 把 ε 等同于 + 号所在的子集 S，平衡即 S 上的 cᵢ 之和恰为总和的一半。cᵢ 全正时，一个平衡子集的真子集和严格更小，所以平衡子集构成反链。对随机最大链计数（LYM 不等式），Σ 1/C(6, |S|) ≤ 1；C(6, k) 的唯一最大值是 C(6, 3) = 20，所以至多 20 个，等号只在全部三元子集都平衡时成立。比较 {a, b, c} 与 {d, b, c} 可知所有 cᵢ 相等。zᵢ²(1 − zᵢ²) = c² 只有两个根 t ≤ 1/2 与 1 − t。若某个 zᵢ² = 1 − t，则其余五个都是 t 时总和 1 − t + 5t = 1 迫使 t = 0，有两个 1 − t 时总和超过 1，都与 zᵢ > 0、Σ zᵢ² = 1 矛盾。所以 zᵢ² = 1/6，wᵢ = 5/6，单位 Gram 为 (6/5)(I₆ − J/6)：对角 1、非对角 −1/5，正是正则五维单纯形的六条中心线。

m = 5. 零坐标的符号是自由的，平衡模式数等于正坐标上平衡子集数乘 2，再按 ±ε 除以 2，所以直线数等于平衡子集数。若某个单独的 cₐ 等于总和一半，平衡子集只有 {a} 与它的补集。否则平衡子集是二元子集及其三元补集。两个平衡二元子集不能不交：否则剩下第五个系数为 0。两两相交的二元子集是星或三角形；在五个点上至多 4 个。所以平衡子集至多 8 个，至多 8 条线。

m = 4. 直线数 = 平衡子集数 × 2² / 2，十条线需要至少 5 个平衡子集。平衡子集在取补下封闭且不等于自己的补集，个数为偶数，所以至少 6 个。四元集上反链至多 C(4, 2) = 6 个，等号只在全部二元子集都平衡时成立，迫使四个正系数相等；同上 zᵢ² = 1/4。这时块由两条与其余向量正交的轴（zᵢ = 0，wᵢ = 1）和其正交补 ℝ³ 中的四条正四面体直线（单位 Gram 非对角 −1/3）组成。另一块的直线在两轴上分量为 ±1/√5，ℝ³ 部分 w 满足 |w|² = 3/5 且与四个四面体方向的内积都是 ±1/√5；解得 w = ±√(3/5)eⱼ，eⱼ 是与四面体对齐的三个坐标方向之一。把 √3 项的符号规定为正，候选线是

(ε₁, ε₂, √3 eⱼ)/√5, ε₁, ε₂ ∈ {±1}, j = 1, 2, 3.

同一 j 下，两条候选的内积是 (ε₁ε₁′ + ε₂ε₂′ + 3)/5：恰差一个 ε 符号时为 3/5，超过 1/√5；两个都不同时为 1/5。所以每个 j 至多两条，不同 j 之间内积绝对值 ≤ 2/5 不受限，总数至多 6 条，不足 10 条。

m = 3. 三个正系数时，平衡子集只在一个系数等于另两个之和时出现，且只有它和补集，至多 2 个。直线数至多 2 × 2³ / 2 = 8。

m ≤ 2. m = 2 时，四条 zᵢ = 0 的线与块内其他线正交且彼此正交（WᵀW 的对应行是 eᵢ），张成 4 维；另外两条线落在剩下的一维正交补中，重合，平方重合度为 1，违反界。m = 1 时 zᵢ = 1，wᵢ = 0，违反 wᵢ > 0；m = 0 与 |z| = 1 矛盾。

结论：6 + 10 只能是正则单纯形的六条线加十条线，第 6 节证明它不能有有理坐标。剩下 (7, 9) 与 (8, 8)。

4. 7 + 9 与 8 + 8：穷举出六个类

记 A 块 p 条线、B 块 q 条线，(p, q) = (7, 9) 或 (8, 8)。从 A 中取五条线性无关的单位向量作为矩阵 U 的行（A 张成 ℝ⁵），X = UUᵀ 是它们的 Gram 矩阵。B 的每条单位向量 b 满足 Ubᵀ = ε/√5，ε ∈ {±1}⁵。翻转 b 可设 ε 的第一个坐标为 +1，于是只有 16 种可能的符号列。U 可逆，所以不同的 B 线对应不同的列；B 张成 ℝ⁵，所以所选的 q 列秩为 5。

A 的其余每条线写成 a = λU（λ 为行向量）。跨块等号条件说 λS ∈ {±1}^q，其中 S 是所选 q 列组成的 5 × q 符号矩阵。取 S 的五个线性无关列组成 E，则 λE ∈ {±1}⁵：逐一试 32 个符号向量、精确解 λ，再检查整行 λS 是否全为 ±1，就得到全部可能的 λ。按整体反号取商，五条基线自身给出五行，再从其余可行行中选 p − 5 行。这一步没有数值优化、抽样或经验剪枝。

行列置换与符号翻转只是重新编号和翻转直线方向，不改变任何内积的绝对值。六个类依次出现 480、1 920、400、1 280、1 160、2 160 次，合计 7 400。类 0–2 为 7 + 9，类 3–5 为 8 + 8。交叉 Gram 矩阵就是 S/√5，所以下一节只需处理六个代表矩阵。

5. 每个类的度量唯一

固定一个代表类，Λ 的第 i 行 λᵢ 是第 i 条 A 线关于基 U 的系数。A 的紧框架恒等式 Σ wᵢaᵢᵀaᵢ = I 写成 UᵀCU = I，即

C = X⁻¹ = Σ wᵢ λᵢᵀλᵢ, Σ wᵢ = 5, λᵢ C⁻¹ λᵢᵀ = |aᵢ|² = 1.

包中每类给出一个精确矩阵 C₀ = Σ wᵢ⁰ λᵢᵀλᵢ（系数在 ℚ 或 ℚ(√5) 中），满足 C₀ 正定、Σ wᵢ⁰ = 5，且每个 λᵢ C₀⁻¹ λᵢᵀ = 1。对任意可行的 C：

tr(C₀⁻¹C) = Σ wᵢ λᵢC₀⁻¹λᵢᵀ = Σ wᵢ = 5, tr(C⁻¹C₀) = Σ wᵢ⁰ λᵢC⁻¹λᵢᵀ = Σ wᵢ⁰ = 5.

记 μ₁, …, μ₅ > 0 为 C₀^(−1/2) C C₀^(−1/2) 的特征值，则 Σ μₖ = 5 = Σ 1/μₖ。由算术–调和平均不等式 (Σ μₖ)(Σ 1/μₖ) ≥ 25，等号当且仅当所有 μₖ 相等，所以 μₖ = 1，C = C₀。于是 X = C₀⁻¹ 唯一确定，A 线的 Gram 矩阵是 ΛXΛᵀ，B 线 bⱼ = U⁻¹Sⱼ/√5 的 Gram 矩阵是 SᵀC₀S/5：16 条线的整个 Gram 矩阵唯一，构型在正交变换意义下唯一。这不依赖任何数值优化。

在唯一度量下逐一检查块内各对（精确的 ℚ(√5) 运算）：

类 0、1、3、4：唯一度量下存在块内平方重合度 9/25 > 1/5 的对，违反相干界，连实构型都不存在。类 5：没有块内对超过 1/5，但 A 块内有一对恰为 1/5，它与任何一条 B 线构成等号三角形，由引理 2.1 不能有有理坐标。类 2：全部块内对都严格小于 1/5，所有对角元为 1，确实是一个实构型（第 1 节的 7 + 9 构型的权重 1/2 与 3/4 与它相同）；它要由第 6 节的算术排除。

6. 有理性障碍

引理 6.1。 若 ℚ⁵ 中有五个两两正交的有理向量，平方范数为 (1, 2, 2, 2t, 2t)，则 t 是两个有理数的平方和。

证明。有理 Householder 反射 I − 2wwᵀ/(wᵀw)（w = x − e₁；x = e₁ 时取恒等）把有理单位向量 x 送到 e₁，并保持有理性与正交性；其余四个向量落入 e₁ 的正交补 ℚ⁴，平方范数 (2, 2, 2t, 2t)。把 ℚ⁴ 看作有理四元数，|pq| = |p||q|。取平方范数为 2 的 q，左乘 q̄/2：它是有理线性映射，把 q 送到 q̄q/2 = 1，把所有内积乘以 1/2，保持正交。平方范数变为 (1, 1, t, t)，第一个就是实单位 1，其余三个在纯虚部 ℚ³ 中。再用一次有理 Householder 把 ℚ³ 中那个单位向量送到坐标轴，剩下的两个向量落在有理坐标平面 ℚ² 内，平方范数为 t：t = x² + y²，x、y 有理。

引理 6.2。 3 和 15 都不是两个有理数的平方和。若 a² + b² = 3c² 或 15c²，取 (a, b, c) 为互素的整数三元组。模 3 的平方只有 0、1，a² + b² ≡ 0 迫使 3 | a 且 3 | b；于是 9 | 3c² 或 9 | 15c²，得 3 | c，与互素矛盾。

公共缩放。 固定任一 B 向量 b。对 A 中两条有理代表 a、a′，s_a s_b = 5(a·b)² 与 s_a′ s_b = 5(a′·b)² 相除，得 s_a/s_a′ = ((a·b)/(a′·b))²，是有理平方。所以对 A 的代表做有理缩放后它们有同一平方范数 s，五条基线（适当取向）的 Gram 矩阵是 sX，与 X 有理合同。五个 ℚ⁵ 有理向量的 Gram 行列式是 det(V)²，是有理平方，所以 s⁵ det X 是有理平方。

类 2。 精确计算 det X = 256/729 = (16/27)²，所以 s⁵ 是平方，s 是有理平方，可再缩放到 s = 1：存在有理 V 使 VVᵀ = X。X 的 LDL 分解 X = LDLᵀ（L 为有理单位下三角）的对角是 (1, 8/9, 8/9, 2/3, 2/3)；L⁻¹V 的行是两两正交的有理向量，平方范数为这些对角元。分别乘以有理数 3/2、3/2、3、3，得平方范数 (1, 2, 2, 6, 6) = (1, 2, 2, 2t, 2t)，t = 3。由引理 6.1，3 是两个有理平方之和，与引理 6.2 矛盾。

正则单纯形（6 + 10）。 取向使六条线两两内积 −1/5，取其中五条为基，X 对角为 1、非对角为 −1/5，det X = (6/5)⁴ · (1/5) = 1296/3125 = 36²/5⁵，LDL 对角 (1, 24/25, 9/10, 4/5, 3/5)。s⁵ det X = 36²(s/5)⁵ 是平方，所以 s/5 是有理平方，可缩放到 s = 5，Gram 为 5X，LDL 对角 (5, 24/5, 9/2, 4, 3)。按平方类有理缩放并重排，得到两两正交、平方范数 (1, 2, 3, 5, 30) 的有理向量。对其中平方范数 3、5 的 u、v，用 (u + v)/2 与 (5u − 3v)/2 替换：平方范数为 (3 + 5)/4 = 2 与 (75 + 45)/4 = 30，内积 (15 − 15)/4 = 0。于是得到 (1, 2, 2, 30, 30) = (1, 2, 2, 2t, 2t)，t = 15，与引理 6.1、6.2 矛盾。（这也是 Schoenberg 与 Pelling 关于有理正则单纯形的经典判据的五维情形：6 不是两个有理平方之和。）

Hasse–Minkowski 交叉验证。 存在有理 V 使 VVᵀ = G 当且仅当二次型 G 与 I₅ 在 ℚ 上等价。不依赖引理 6.1，也可以直接比较不变量：类 2 的 X 与单纯形的 5X 行列式都在平方类 1 中、都正定，但它们的 Hasse 不变量在 p = 2 与 p = 3 处都与 I₅ 不同，所以都不与 I₅ 有理等价。同样 Hilbert 符号 (−1, 3)ₚ = (−1, 15)ₚ = −1（p = 2、3），独立地确认 3 与 15 不是两个有理平方之和。

7. 网格上的结论

第 2–6 节排除了有理坐标下 q = 1/5 的每一种可能：块数恰为二（§2），大小不是 5 + 11，6 + 10 只能是正则单纯形（§3），7 + 9 与 8 + 8 只剩六个类（§4），其中五个由唯一度量排除（§5），类 2 与单纯形由算术排除（§6）。结合命题 1.2，任意有理坐标的 16 条直线都有 q > 1/5 严格成立，所以 10¹⁸q > 2 · 10¹⁷，

K = ceil(10¹⁸ q) ≥ 200000000000000001.

这个下界可以达到。包中九位小数答案的 120 对平方重合度精确计算后，最大值为

q = 31903962418344681393274995137809561 / 159519812091723406674694957320312413,

它比 1/5 大约 3.66 × 10⁻¹⁹，所以 K = 200000000000000001，页面显示 μ = 0.447213596。这等于本站当前纪录，所以纪录就是网格最优值。“有理点达不到 1/5”与“整数分数达到最小值”并不矛盾：向上取整把 (1/5, 1/5 + 10⁻¹⁸] 中的所有 q 记为同一个分数。

我们的核验

证明包由 zzzcy #308 于 2026 年 10 月 6 日通过邮件提交，投稿时注明借助 AI 生成。按本站规定，我们没有运行包中的任何脚本，只读取数据文件。第 1–3、5–7 节的手写论证由我们逐行检查；有限的计算部分由本站自己的程序 tools/p60-certificates.py 用精确有理数和自写的 ℚ(√5) 运算重放，约 2 分钟：

• 自己做第 4 节的穷举：24 310 个列子集，24 290 个秩为 5，6 210 个有足够的可行行，7 400 个原始矩阵，与包中见证文件的集合完全相同。
• 7 400 个行列置换加符号翻转的见证逐项作用到原始矩阵上，都落到六个代表之一，出现次数 480、1 920、400、1 280、1 160、2 160。
• 每个类在精确 ℚ(√5) 中重建 Λ，验证 C₀ = Σ w⁰λᵀλ、Σ w⁰ = 5、正定性与单位对角，再由唯一度量重建两块的 Gram 矩阵：类 0、1、3、4 有块内 9/25，类 5 有 A 内恰为 1/5 的对，类 2 在 ℝ 上可行。
• 类 2（det 256/729，LDL 1, 8/9, 8/9, 2/3, 2/3）与单纯形（det 1296/3125，缩放为 5X）的障碍由 LDL 与行列式复核，并独立地由 Hasse–Minkowski 不变量复核（在 p = 2、3 处与 I₅ 不同）；(−1, 3)ₚ = (−1, 15)ₚ = −1（p = 2、3）。
• 第 3 节的有限论断穷举：5 + 11 情形中 (±1, …, ±1)/√5 型直线两两内积 ±1/5 的最大族是 5 条；m = 4 情形的候选线最多相容 6 条；各 m 的平衡子集最大数 2、6、8、20 也做了整数权重的健全性检查。
• 包中答案精确计分：q = 31903962418344681393274995137809561/159519812091723406674694957320312413，分数 200000000000000001。

重放命令：python tools/p60-certificates.py <证明包目录>，结果 PASS。

两处文字更正。 两处都不影响证明的成立，本页已按更正后的说法写出。(1) 包中证明第七节说类 0、1、4 的违反值是 9/25，而这三类的证书点名的是一对 1/4；两者都大于 1/5，唯一度量下的最大值确实是 9/25。(2) 包中第五节 m = 4 情形说“只差一个符号的两条线内积为 3/5”，这只在先把 √3 项的符号固定为正之后成立（若翻转的是 √3 项的符号，内积是 −1/5）；结论“每个 j 至多两条、共至多 6 条”正确，我们已穷举确认。另外，5 + 11 情形的计数界给出至多 6 条，实际最大值是 5 条，两者都远小于 11。

贡献与范围

μ² ≥ 1/5 是 R. A. Rankin（1955）的正交多面体界，投影矩阵的写法见 Conway、Hardin 与 Sloane（1996）；16 条线取到 1/√5 的构型早已知道，收录在 Henry Cohn 的 Grassmannian 打包档案中。本证明的新内容是 (b)：有理坐标达不到 1/5，所以本站当前纪录 200000000000000001 就是九位小数网格上的最优值，纪录持有者不变。本项采纳的贡献记 zzzcy #308 一次永久 +2 证明分。

Cohn · Conway–Hardin–Sloane · 查看 P60