Superpermutation Almanac

S(8) ≥ 46,130

Holds for: n = 8
Announced: Sep 4, 2026
Proof: Lean proof, relying on native_decide
Points: 1.5The Lean proof relies on native_decide and earned half points.

By William Echols.

Evidence

Lean proof, native-checked github.com/williamechols/superperm8-ge-46130 Commit 893ab2d92669ea56d012ceca626bf01ca631e920 Lean proof generated by GPT-6 Astra (Extra High effort), building on Lebar and Grayzel; uses native_decide

Proof check

native-checked

LowerBoundAt 8 46130

Linking lemma written by the Almanac.