S(7) ≥ 5,898
S(7) ≥ 5,898
- Holds for
- n = 7
- Announced
- Aug 13, 2026
- Proof
- Lean proof
By Justin Lebar.
Evidence
-
Lean proof, native-checked
github.com/jlebar/superperm7-ge-5898
Commit
f516e19b232079947027698c1447009f929ed28cSuperperm7.main_theorem; branch-and-bound over trails with 380 certificates via native_decide; generated with an unreleased Claude model; builds on Grayzel's superperm6
Historical proof checks
These checks cover the bound’s mathematical statement. The paper and source notes are for citation.
native-checked
LowerBoundAt 7 5898Original job: local-lebar-20261027-cached-eight. Original policy: 1cbf746d45c9dc6bc771974aab0597aec6acce08736539af0e02a2b619560836.
Linking lemma written by the Almanac.