S(10) ≥ 4,033,379
S(10) ≥ 4,033,379
- Holds for
- n = 10
- Announced
- Oct 29, 2026
- Proof
- Lean proof
By Jay Pantone 
Evidence
-
Lean proof, kernel-checked
github.com/jaypantone/2026-10-superpermutation-lower-palomar at commit
ad72ab5010e945b5c8768a918281778c834dcc40Paper: finite/finite-lower-bounds.pdf (+18 files) Checked on Oct 29, 2026.
Proof checks
kernel-checked
- Checked
- Oct 29, 2026
- Lean version
- leanprover/lean4:v4.35.0
- Mathlib commit
56a005855ea17e0b0958f73ec801ae140b0a1679- lean
v4.35.0- lean4checker
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc- nanoda
lean4-bundled@eb6cafb7290e8bd5f2937522d8d804f58f02bafc
build 993 s, peak 7.5 GB
Result 2 of batch L-0015, theorem lower10, checked in attempt 1: AlmanacSolution.lean, line 13.
theorem lower10 : Almanac.LowerBoundAt 10 4033379Repository at the checked commit · Repository archive (17.6 MB)
The judge checks each proof with two kernels. A fixed statement is also compared with the Almanac’s definitions; a custom statement is reviewed by hand.