S(7) ≥ 5,898
- Holds for
- n = 7
- Announced
- Nov 10, 2026
- Proof
- Lean proof
- Points
- 1.8
By 
Evidence
-
Lean proof, kernel-checked
github.com/jhalfar/superpermutation-almanac-lean at commit
5cc0ac3e8954e4de58feb4d12a4a9d5f3c897c11Checked on Nov 10, 2026.
Proof check
kernel-checked
- Checked
- Nov 10, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 3153 s, peak 17.6 GB
Result 1 of batch L-0023, theorem lower_seven, checked in attempt 1: AlmanacSolution.lean, line 10.
theorem lower_seven : Almanac.LowerBoundAt 7 5898Repository at the checked commit · Repository archive (6.4 MB)
The proof of 5,898 uses the first step of my 5,899 proof from proofs/lean/n7 in my main repository: at cost 133 the chain caps and the five profile statements alone are enough. All searches are checked by the kernel, without native_decide.