| n | 连续最优值的包围区间 | 九位小数最优值（精确） |
|---|---|---|
| 1 | [0.688190960235586769103604790955, 0.688190960235586769103604790956]√(25 + 10√5)/10 | 0.688190959 |
| 2 | [0.760845213036122857693151466703, 0.760845213036122857693151466704]√(10 + 2√5)/5 | 0.760845212 |
| 3 | [1.034563887852745238722502573982, 1.034563887852745238722502573983] | 1.034563887 |
| 4 | [1.250988879234854835726034468650, 1.250988879234854835726034468651] | 1.250988878 |
| 5 | [1.447980550405670367298603865867, 1.447980550405670367298603865868]5/(2√(5 − 2√5) + 2) | 1.447980549 |
| 6 | [1.651074770596782374034569505953, 1.651074770596782374034569505954](4 + 1/sin 36°)/(2√(5 − 2√5) + 2) | 1.651074767 |
| 7 | [1.740983299207393612609980566106, 1.740983299207393612609980566107] | 1.740983297 |
| 8 | [1.852488899111271345913487762578, 1.852488899111271345913487762579] | 1.852488896 |
不能直接把连续最优值截断作为格点最优。例如 n = 6 的截断值是 1.651074770，但圆心同时受格点限制，可达到的最大值是 1.651074767。n = 3–8 的连续最优构型还证明了唯一性：只允许正五边形的对称变换和圆的重新编号。这里不主张格点最优构型唯一，也不涉及 n ≥ 9。
证明思路
记内切圆半径 a = cot(π/5)/2、外接圆半径 R = 1/(2sin(π/5))。半径 r 的圆心可行域是缩小的正五边形 (1−r/a)P。一个圆有 r ≤ a。对两个圆，由圆心距至少为半径和，以及三角不等式，可得 S ≤ R(2−S/a)，故 S ≤ 2aR/(a+R)；内切圆加一个角落圆取等。
n = 3、5、6 的候选构型用根式精确给出；n = 4、7、8 用接触方程组与有理隔离盒定义。区间计算验证 Banach 不动点条件、正半径、所有边界条件和未指定接触的间隙，从而证明精确根存在且构型合法。
全局部分选取最长圆心对，以五边形对称将其方向归入 [π/10,3π/10]，枚举其余圆心位于直线两侧的数量。n = 3–6 在同侧按半径排序；n = 7–8 改为按极角排序。方向区间被完整细分，每个真实构型都保留一条根到叶路径。边界、方向、分离距离和先前已证明的子集上界给出必要的线性约束。
对于 Az ≤ b 和已知变量盒 B，任何非负有理向量 y 都给出 c·z ≤ y·b + max(z∈B)(c−Aᵀy)·z。验证器用向外舍入的有理区间重新计算右侧，包括全部系数残差；优化器报告“不可行”并不算证明。每个分支必须完整，普通叶必须有严格上界或矛盾证书。
其余叶证明所有有竞争力的构型距离候选根足够近。把非零扰动除以其最大分量后，至少一个归一化分量的绝对值为 1；带严格 Taylor 余项的局部模型却证明所有分量都小于 1，从而排除同分或更优的不同构型。这完成连续全局最优性证明。
格点证明回到本站未经旋转的坐标系，对全部 10 个对称方向逐一检查整数邻域；n = 5 的圆集合本身具有全部对称性，只需一个邻域。整数分支及严格矛盾证书排除所有分数至少为下一格的构型。最后，8 份坐标由本站原有精确验证器检验，达到表中的格点上界。
复验材料
SHA-256: d7f8c7b77179193dd6bcd8d76619c2d88765257791f4538e4559bf722bc99ddd
python verify_proofs.py --output replay_result.json使用 Python 3.10 或更新版本，不使用 -O 或 -OO。只依赖标准库；预留至少 4 GB 临时磁盘空间。--quick 只检查文件完整性和构型，不是完整证明复验。支持 fork 和 pread 的系统可添加 --workers 3。
本站审查了几何归约、区间运算、局部刚性和格点排除代码，并从头运行投稿附带的验证程序，没有复用旧审计结论。Windows 单进程复验耗时约 28 分钟；n = 8 的 1,044,679 个全局节点和 353,596 个格点节点全部通过。另用本站现有验证器检查了全部构型。这是计算机辅助证明审查，不是证明助理内核的形式化验证。
署名与采纳
证明由 zzzcy #308 投稿，本站完成审查和双语整理，按一项贡献计 +2 证明分。已有构型保留 Friedman 表中的 Jonathan Viquerat 等发现者署名；两圆连续结论已有 Ninjbat（2016）的一般性定理。本页不主张首次发现这些构型或数学史上的首次证明。
Erich Friedman: Circles in Pentagons · Ninjbat (2016)
n = 1–8 按“已证明最优”停止竞赛，保留历史提交和纪录持有人。证明附件中的坐标不会自动替换玩家纪录。