| s(k² − 3) = k for every k ≥ 6 | certificates/k2m3/ | certificates/k2m3/verify.sh [--full] | /k2m3/ | in the kernel with no hypothesis (valid7, bentz; wand125's PR #6, merged 10-10; root modules built by wand125, not rebuilt here: tasks/pr6-valid7-kernel/); all-k reduction bentz_of_validTilt7 |
| s(k² − 4) = k for every k ≥ 5 | certificates/k2m4/ | certificates/k2m4/verify.sh [--full] | /k2m4/ | all-k reduction bentz4_of_validTilt9, conditional on the tilted box statement (re-checked by wand125's separate exact checker, 10-06; not yet register-verified) |
| s(60) = s(61) = 8 | certificates/s60/ | certificates/s60/verify.sh [--full] | /s60/ | — |
| s(45) = 7 | certificates/s45/ | certificates/s45/verify.sh [--full] | /s45/ | — |
| s(32) = 6 | certificates/s32/ | certificates/s32/verify.sh [--full] | /s32/ | s32_eq_6, no hypothesis (opt-in build) |
| s(21) = 5 | certificates/s21/ | certificates/s21/verify.sh [--full] | /s21/ | s21_eq_five_of_checker, conditional |
| s(13) = 4, case-free | certificates/rung2/ | ./verify.sh | /s13/ | s13_eq_4, no hypothesis (opt-in build) |
| s(12) ≥ 15680/3951 = 3.9686 (squarepacker's 3.9715 re-weights these points) | certificates/ s12_lower_3.9686.txt | ./verify.sh | /s12/ | s12_ge_15680_3951, no hypothesis (opt-in build) |
| s(11) ≥ 3040/797 (superseded: s(11) = 3.877… is now proved) | certificates/ s11_lower_3.8143.txt | ./verify.sh | /s12/ | s11_ge_3040_797, no hypothesis (opt-in build) |
| s(n² − n + 1) < n for every n ≥ 15 (Kevin Fang, jlevy#603) | certificates/fang-gluing/ | certificates/k2-minus-c/verify.sh --fang | /k2c/ | FangFinal.theorem1/2, no hypothesis (opt-in build) |
| c(k) ≤ 4⌈√(2k − 7)⌉ − 1* (k ≥ 7) and c(k) < 18.9 k^{2/5} + 35.7 k^{1/5} + 122* (k ≥ 3·10⁵); Ryu's 8⌈√(k − 4)⌉ − 1 and his Theorem 1.2 (k ≥ 8·10⁶) | certificates/k2-minus-c/ | certificates/k2-minus-c/verify.sh | /k2c/ | RyuLayers, RyuStairBound, RyuBound; no hypothesis |
| R₃ exactly: three unit squares (any angles) fit in w × h iff both sides ≥ 1 and (both ≥ 2, or one ≥ 3, or ℓ + 2s ≥ 4 + 2√2 with short side s < 2: the 45° wedge). The boundary and its constructions, wedge included, are from Erich Friedman's Math Magic, June 2010 (boundary of S₂; solvers of that problem: Morandi, Stenlund, Cantrell, Hosono); new here is the proof, the first we know of (Yang 2026 leaves part of the region open) | — | cd lean && lake build Sqpack.Rect3 | search/rectfront/RECTFRONT.md | rect3_iff, no hypothesis (also rect2_iff, R₂) |
R₄ exactly: four unit squares (any angles) fit in w × h iff both sides ≥ 1 and (both ≥ 2, or one ≥ 4, or, with short side s < 2, ℓ ≥ L(t, s) = 2 + (1 − 2(s − k − 1) sin t)/cos t + (1 − (s − 2k) cos t)/sin t, k = (cos t + sin t)/2, for some t: two uprights in opposite corners and a tilted pair between them). The boundary and its constructions are from Erich Friedman's Math Magic, June 2010 (boundary of S₃; its tilted piece credited there to MM, i.e. Maurizio Morandi; closed form also in wand125's problems/rectangles k = 4); new here is the proof (chain of shelves; the separating line of the middle pair gives t) | — | cd lean && lake build Sqpack.Rect4 | search/rectfront/RECTFRONT.md | rect4_iff, no hypothesis |
R₅ exactly: five unit squares (any angles) fit in w × h iff both sides ≥ 1 and (one side ≥ 5; or both ≥ 2 and (one ≥ 3 or w + h ≥ 4 + √2, the stretched s(5) packing, so s(5) = 2 + 1/√2, Göbel 1979); or, with short side s < 2, ℓ + 4s ≥ 4 + 6√2: the 45° zigzag). The boundary and its constructions are from Erich Friedman's Math Magic, June 2010 (pieces 4.1–4.5 of S₄, all credited there to MM, i.e. Maurizio Morandi; closed forms also in wand125's problems/rectangles k = 5); new here is the proof: weighted point covers for both sides ≥ 2 (incl. a 10-point 2/3–1/3 cover), and, for strips (s < 2), the odd-n strip theorem at n = 5 (strip_odd_lower; below height 1.87, monotonicity: the zigzag there already needs length > 5). The first strip proof, ~14k lines of generated certificates, is archived in search/rectfront/r5strip/lean-attic/ | — | cd lean && lake build Sqpack.Rect5Iff (~2 min, ~4 CPU-min) | search/rectfront/RECTFRONT.md, r5strip/FINAL5.md, r5pts/R5PTS.md | rect5_iff, no hypothesis |
Low strips, every n: n unit squares in L × H with H < 2√2 − 1 ≈ 1.828 need L ≥ n (n − 1 midline points (i, H/2), generalising rect5_low; sharp as n → ∞, since the tilted strip pieces start just above 2√2 − 1) | — | cd lean && lake build Sqpack.StripLow | search/rectfront/RECTFRONT.md | strip_low, no hypothesis |
Odd n in a strip, H(9) ≤ H < 2, exactly* (H*(9) = (14√2 − 5)/8 ≈ 1.8499; so n = 3, 5, 7, 9 exactly for every strip): for odd n ≥ 3, n unit squares fit in L × H iff L ≥ n or L ≥ (n − 2)(2√2 − H) + 4 − H (the 45° zigzag; boundary pieces in Friedman's Math Magic, June 2010, for n ≤ 9, and wand125 problems/rectangles for n ≤ 15). New here: the proof for every odd n — packings become a walk on separating-line slopes with an explicit per-square cost, bounded by parity prefix potentials (below 1.87: tangent potentials; one square against one line is extreme at a horizontal, breakpoint or aligned line, leaving a table of 39 line pairs and 163 generated polynomial leaves) | — | cd lean && lake build Sqpack.StripBandMain | search/rectfront/RECTFRONT.md | strip_odd_iff, strip_odd_iff', strip_odd_iff_le9, no hypothesis |
Exact forms of the record packings, n ≤ 324 (S* as an algebraic number; Lean Packs n S*; local minimality) | search/exact/ | search/exact/batch/verify_all.sh | EXACT_FORMS.md | lean/Sqpack/Exact/ |
| New record packings: s(266), s(270), s(272) upper bounds | search/exact/results/sw2/ | search/exact/verify_cert.py | — | — |
| Packings beating the 2×2 doublings of the s(241), s(273), s(307) records: s(964) ≤ 31.8595, s(1092) ≤ 33.8406, s(1228) ≤ 35.8474 (evidence for "tilings are never optimal") | search/tilings/ | search/exact/verify_cert.py, verify_cert2.py | search/TILINGS.md | conjecture stated: Conjectures.TilingsNeverOptimal |
