S(8) ≥ 46,133
S(8) ≥ 46,133
- Holds for
- n = 8
- Announced
- Oct 6, 2026
- Proof
- Lean proof
By Jakub Halfar.
Evidence
- Lean proof github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean Theorem C: kernel-checked finite search (827,022 states at n = 8), 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
LowerBoundAt 8 46133Original job: historical-20261025-194320-276bc4e5-halfar-n8. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.
Linking lemma written by the Almanac.