The 926683/1814400 bound
For large n, S(n) \le n! + (n-1)! + (n-2)! + \left(926683/1814400 + \varepsilon\right)(n-3)!
- Holds for
- large n
- Announced
- Oct 28, 2026
- Proof
- Lean proof
- Coefficient of (n−3)!
- 926683/1814400
By Jay Pantone 
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/2026-10-superpermutation-upper-palomar at commit
d771f355ab604950ceb417346764707952e0b9e7Paper: upper/upper-bounds.pdf (+1 file) Checked on Oct 29, 2026.
Proof checks
kernel-checked
- Checked
- Oct 29, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean
v4.35.0- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 2258 s, peak 14.9 GB
Result 1 of batch L-0014, theorem asymptotic_upper, checked in attempt 2: AlmanacSolution.lean, line 9.
theorem asymptotic_upper : Almanac.AsymptoticUpper (926683/1814400)Repository at the checked commit · Repository archive (50.9 MB)
The judge checks each proof with two kernels. A fixed statement is also compared with the Almanac’s definitions; a custom statement is reviewed by hand.