Jay Pantone's bound
For large n, S(n) \ge n! + (n-1)! + (n-2)! + \left(2 - \varepsilon\right)(n-4)!
- Holds for
- large n
- Announced
- Oct 29, 2026
- Proof
- Lean proof
By Jay Pantone 
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/2026-10-superpermutation-lower-palomar at commit
ad72ab5010e945b5c8768a918281778c834dcc40Paper: finite/finite-lower-bounds.pdf (+18 files) 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 993 s, peak 7.5 GB
Result 5 of batch L-0015, theorem asymptotic_lower_four, checked in attempt 1: AlmanacSolution.lean, line 22.
theorem asymptotic_lower_four : Almanac.AsymptoticLowerAt 4 2Repository at the checked commit · Repository archive (17.6 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.