Kisic's bound

For every n ≥ 5, S(n) \ge n! + (n-1)! + (n-2)! + n - 3 + \left\lceil \frac{2((n-2)! - (n-2))}{n(n-3)} \right\rceil

Holds for: n ≥ 5
Announced: Oct 6, 2026
Proof: Lean proof
Coefficient of (n−3)!: 0

By Marin Kisic and Jakub Halfar. Posted by Kisic as unverified (2026-08-07); proved in Lean by Halfar (2026-10-06).

Values

n	At least
5	153
6	870
7	5,893
8	46,121
9	408,433
10	4,033,159
11	43,916,736
12	522,614,409
13	6,746,553,315
14	93,890,534,411

Evidence

Preprint github.com/mkisic/superpermutations lower_bound_unverified.pdf, produced with GPT 5.6 Sol Pro; posted by Kisic as unverified
Lean proof github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditA.lean Theorem A, proved in Lean by Jakub Halfar on 2026-10-06 (no native_decide)
Lean proof, kernel-checked github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower Commit cc5c763bd5854317b20dadb138990802656e6f03

Historical proof checks

These checks cover the bound’s mathematical statement. The paper and source notes are for citation.

kernel-checked

LowerBoundFrom 5 (.add (.sub (.add (.add (.add (.fact 0) (.fact 1)) (.fact 2)) (.var)) (.const 3)) (.div (.mul (.const 2) (.sub (.fact 2) (.sub (.var) (.const 2)))) (.mul (.var) (.sub (.var) (.const 3)))))

Original job: historical-20261025-143453-f94580fe-kisic-headline. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.

Linking lemma written by the Almanac.