S(9) ≥ 408,470
- Holds for
- n = 9
- Announced
- Nov 10, 2026
- Proof
- Lean proof, relying on
native_decide - Points
- 0.0The Lean proof relies on
native_decideand earned half points.
By 
Evidence
-
Lean proof, native-checked
github.com/williamechols/superpermutations at commit
464e5fa54e0638a6d62c19c0d7e373c6bc3dd5b1Checked on Nov 10, 2026.
Proof check
native-checked
- Checked
- Nov 10, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 814 s, peak 4.5 GB; native_decide re-evaluation 801 s
Result 1 of batch L-0022, theorem lower_nine, checked in attempt 1: AlmanacSolution.lean, line 8.
theorem lower_nine : Almanac.LowerBoundAt 9 408470Repository at the checked commit · Repository archive (714.4 kB)