S(6) ≥ 872

Evidence

• Lean proof, native-checked github.com/BGray-wrl/superperm6 Commit d8a932d8f61d80b0bcfc737bd0e235a8300449c4 end-to-end Lean 4 proof that s(6) = 872, uses native_decide; Grayzel reports a two-person audit of the statement (2026-08-14)
• Preprint github.com/BGray-wrl/superperm6/blob/main/paper/superperm6.pdf 18-page write-up generated against the Lean proof

Historical proof checks

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

native-checked

LowerBoundAt 6 872

Original job: historical-20261025-081650-30772146-grayzel-n6. Original policy: beee848f6a70e956ef67f67b8fc957d8766f7123d24bdfada422eb91e1b43947.

Linking lemma written by the Almanac.