S(9) ≥ 408,469
S(9) ≥ 408,469
- Holds for
- n = 9
- 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 with a kernel-checked finite search
-
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 9 408469Original job: historical-20261026-071203-b9514d1c-halfar-n9. Original policy: d5ef26408bfac3533cf01bb992ecd3256c94be63c2b91dddc40ab53fbf08fd2e.
Linking lemma written by the Almanac.