S(7) ≥ 5,899

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

By Jakub Halfar.

Evidence

Lean proof, native-checked github.com/jhalfar/superpermutation-almanac-lean at commit a09f9ef4ebb74ae1297f17c5fad38296695f2959 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 876 s, peak 19.8 GB; native_decide re-evaluation 288 s

Result 1 of batch L-0020, theorem lower_seven, checked in attempt 1: AlmanacSolution.lean, line 10.

theorem lower_seven : Almanac.LowerBoundAt 7 5899

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

My proof of 5,899 from proofs/lean/n7 in my main repository, with twelve finite searches by native_decide. Six of them run on the newer search engine of proofs/lean/n7_5900 and n7_5901.