The 3/5 bound
For every n ≥ 10, S(n) \le n! + (n-1)! + (n-2)! + \tfrac{3}{5}(n-3)!
- Holds for
- n ≥ 10
- Announced
- Sep 29, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 3/5
By Jay Pantone jaypantone.
Values
| n | At most |
|---|---|
| 10 | 4,035,024 |
| 11 | 43,932,672 |
| 12 | 522,764,928 |
| 13 | 6,748,116,480 |
| 14 | 93,908,263,680 |
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/superperm-upper-43-80
Commit
c8fb7ffdd69be1375580710ae11b47a295b1f0f6'earlier uniform bound' proved in the repository's Lean library
Historical proof checks
These checks cover the bound’s mathematical statement. The paper and source notes are for citation.
kernel-checked
UpperBoundFrom 10 (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.div (.mul (.const 3) (.fact 3)) (.const 5)))
Original job: historical-20261025-143453-f94580fe-pantone-3-5. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.
Linking lemma written by the Almanac.