S(7) ≥ 5,897
- Holds for
- n = 7
- Announced
- Nov 9, 2026
- Proof
- Lean proof
- Points
- 3.1
By 
Evidence
-
Lean proof, kernel-checked
github.com/williamechols/superpermutations at commit
0a9bbfc5d8d3066e2668681b48cd717209cc9706Checked on Nov 9, 2026.
Proof check
kernel-checked
- Checked
- Nov 9, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 846 s, peak 8.7 GB
Result 1 of batch L-0019, theorem lower_seven, checked in attempt 1: AlmanacSolution.lean, line 8.
theorem lower_seven : Almanac.LowerBoundAt 7 5897Repository at the checked commit · Repository archive (921.0 kB)