4chan + 1
For every n ≥ 5, S(n) \ge n! + (n-1)! + (n-2)! + n - 2
- Holds for
- n ≥ 5
- Announced
- Nov 2, 2018
- Proof
- Lean proof
- Coefficient of (n−3)!
- 0
By Robin Houston. Improves the 4chan bound (Anonymous, Houston, Pantone and Vatter) by one.
Values
| n | At least |
|---|---|
| 5 | 153 |
| 6 | 868 |
| 7 | 5,885 |
| 8 | 46,086 |
| 9 | 408,247 |
| 10 | 4,032,008 |
| 11 | 43,908,489 |
| 12 | 522,547,210 |
| 13 | 6,745,939,211 |
| 14 | 93,884,313,612 |
Evidence
- Paper doi.org/10.1080/00029890.2021.1835384 Engen and Vatter (2021), after Theorem 2.5: 'Houston has shown (in the Superpermutators group) that the bound in Theorem 2.5 can be increased by 1'; stated, not reproved
-
Lean proof
github.com/urdvr/superperm-coeff2
Commit
12acadf0069dd4098a6cacec2dff21b6c8096a18Raudvere's Lean theorem Coeff2.intromain (2026-07-18) gives S(n) ≥ HPV(n) + ⌈((n−3)! − 1)/(2n − 1)⌉ for n ≥ 5, which is at least this bound; the k = 0 case of its criterion is this bound