S(8) ≥ 46,134

Holds for: n = 8
Announced: Nov 8, 2026
Proof: Lean proof, relying on native_decide
Points: 0.3The Lean proof relies on native_decide and earned half points.A proof of this bound without native_decide would earn 0.3 more points.

By Jakub Halfar.

Evidence

Lean proof, native-checked github.com/jhalfar/superpermutation-almanac-lean at commit 7e6664d7b15ed56580cb51cafd8354c3b26a20b9 Checked on Nov 9, 2026.

Proof check

native-checked

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

build 3471 s, peak 8.2 GB; native_decide re-evaluation 3022 s

Result 1 of batch L-0017, theorem lower_eight, checked in attempt 3: AlmanacSolution.lean, line 10.

theorem lower_eight : Almanac.LowerBoundAt 8 46134

Repository at the checked commit · Repository archive (749.9 kB)

Theorem D from proofs/lean/n8_46134 in my main repository. Three finite searches run by native_decide. The kernel checks everything else, including the proof that a search with no hits implies the bound. Without native_decide, the same libraries give 46,133 (Theorem C in proofs/lean/lower), which is the bound already listed.