S(12) ≥ 522,622,380
S(12) ≥ 522,622,380
- Holds for
- n = 12
- 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 3 of batch L-0015, theorem lower12, checked in attempt 1: AlmanacSolution.lean, line 16.
theorem lower12 : Almanac.LowerBoundAt 12 522622380Repository 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.