S(6) ≥ 872

Holds for: n = 6
Announced: Nov 8, 2026
Proof: Lean proof
Points: 28.2

By Jakub Halfar.

Evidence

Lean proof, kernel-checked github.com/jhalfar/superpermutation-almanac-lean at commit 7b7b96dd3c8c9b83cb517e370deaec58cff5b6f6 Checked on Nov 8, 2026.

Proof check

kernel-checked

Checked: Nov 8, 2026
Lean version: leanprover/lean4:v4.35.0
Mathlib commit: 56a005855ea17e0b0958f73ec801ae140b0a1679
lean4checker: lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
nanoda: lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc

build 1229 s, peak 10.1 GB

Result 1 of batch L-0018, theorem lower_six_kernel, checked in attempt 1: AlmanacSolution.lean, line 9.

theorem lower_six_kernel : Almanac.LowerBoundAt 6 872

Repository at the checked commit · Repository archive (1.8 MB)

The proof from proofs/lean/small in my main repository, checked by the kernel alone, without native_decide. Here its two finite searches are cut into 319 small pieces (K6/Frontier.lean) so that the kernel check fits the judge's memory limit. The 872 already listed is Benjamin Grayzel's native_decide proof. This one doesn't use his code.