Jay Pantone's bound
For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(2 + \varepsilon\right)(n-4)!
- Holds for
- large n
- Announced
- Nov 9, 2026
- Proof
- Lean proof
- Coefficient of (n−4)!
- 2
- Points
- 0.0
By 
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/2026-10-superpermutation-asymptotics at commit
882721e53a9e4927dba06921a5efb8e817563464Paper: manuscript.pdf · assembly.tex · geometry.tex · global.tex (+3 files) Checked on Nov 9, 2026.
Proof check
kernel-checked
- Checked
- Nov 9, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 623 s, peak 5.0 GB
Result 1 of batch L-0021, theorem asymptotic_upper_four, checked in attempt 1: AlmanacSolution.lean, line 11.
theorem asymptotic_upper_four : Almanac.AsymptoticUpperAt 4 2Repository at the checked commit · Repository archive (2.2 MB)