Jakub Halfar's 8*(n-4)! asymptotic upper bound
For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(8 + \varepsilon\right)(n-4)!
- Holds for
- large n
- Announced
- Nov 8, 2026
- Proof
- Lean proof
- Coefficient of (n−4)!
- 8
- Points
- 0.0
By 
Evidence
-
Lean proof, kernel-checked
github.com/jhalfar/superpermutation-almanac-lean at commit
af99e8317297566e7bd33fb69bc10c44c484fdc3Checked on Nov 8, 2026.
Proof check
kernel-checked
- Checked
- Nov 8, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 251 s, peak 3.8 GB
Result 2 of batch L-0016, theorem upper_coeff4, checked in attempt 1: AlmanacSolution.lean, line 15.
theorem upper_coeff4 : Almanac.AsymptoticUpperAt 4 8Repository at the checked commit · Repository archive (318.4 kB)
Pantone's 43/80 construction with nested block levels added, built on his Lean library. First in proofs/lean/constant43586371 of my main repository.