T-153: Candidate proof that Bidwell's 1998 packing is optimal, $s (17) = 4.67553009360455 \dots$

V0 C1 Optimality reviewed

2026-10-12 published · Overbeck after Levy, Ahmed, Mira-acc, Guzhou0806, Maaz · $n = 17$

Overbeck (Kleddamag) claims, as a candidate proof, that $s (17) = L = 4.67553009360455095163 \dots$ , the side of Bidwell's 1998 packing of seventeen unit squares, with the squares closed, independently rotated and allowed to touch.

His STATEMENT.md defines $F (t, b) = t - 3 t^{2} - t^{3} - t^{4} + (1 - t - t^{4} + t^{5}) b + (- 3 t + t^{2} - t^{3} - t^{4}) b^{2}$ and $G (t, b) = - 2 t^{3} - 2 t^{4} + (- 1 + 3 t - 4 t^{2} + t^{4} + t^{5}) b + (4 - 2 t - 2 t^{2} + 2 t^{3} - 2 t^{4}) b^{2} + (- 1 - 5 t + 4 t^{2} + t^{4} + t^{5}) b^{3} + (2 t + 2 t^{2}) b^{4}$ , takes $t_{0}$ and $b_{0}$ to 60 places.

It states, its TeX written out: "There exists exactly one simultaneous real zero $(t^{*}, b^{*})$ in the isolating rectangle [t0 - 10^-12, t0 + 10^-12] x [b0 - 10^-12, b0 + 10^-12]. Set L = (6+4t*)/(1+2t*-t*^2); its denominator is positive and $4.67553009360455095163 < L < 4.67553009360455095164$ . There exists a packing of seventeen unit squares at side $L$ , and for every S >= 0, existence of such a packing at side S implies L <= S. Uniqueness of an optimal packing is not claimed."

The claim is conditional. STATEMENT_STATUS.md says to read it as holding "if the 210 obligations of OBLIGATIONS.json hold", 15 of them mathematical premises, and calls it "the claim of a candidate proof, not an established theorem". Its five steps are the upper bound; capture at side at most 4675531/10^6 by 98 weighted counting certificates, leaving 11 cases; admission of each case into one of 11 regions; 13 tree certificates, by which ten regions hold no packing below L and the eleventh only packings in a tube around the known one; and a rigidity step, 17 exact rounds and a contraction of ratio 159201934153319/200000000000000.

Its audit was by AI sessions; Guzhou0806 read the premises in an earlier state and ran a checker of his own on two of the 13 trees, and nobody outside has verified the whole.

Here the argument has been read by three separately prompted AI review lanes, with no mathematical defect found in what was read, and parts of the computation have been run, all agreeing with the source: the author's check.py; 34 capture rows and three trees, reproduced with the producer's code; and, by independent implementations, a sample of 34 capture rows and one of the 13 trees, JQ, and in full the root, the normalized 52-row gate of the rigidity step, the upper construction with its contacts, the root admission, the literal facts of the capture step and the hand-overs. The complete capture recomputation and ten trees have not been run.

F, G, the rectangle and the side map are this repository's H-255 chart, so L is the side of the certified endpoint that holds the case's verified upper bound.

Overbeck, the-seventeenth-square-candidate, 12 October 2026, building on Squares Project (Levy), Ahmed's 11SquaresOptimal, Mira, Guzhou0806's N17 project and Maaz, as its CREDITS.md states. Its README says: "The mathematics, the engines, the certificates, the checkers, the reviews and the text were produced by AI systems under his direction and to his instructions: Codex (OpenAI) and Claude (Anthropic). They are named and are not authors", and "Within the project no human has read the mathematics."

Significance, composition and next rung

Significance: Scored as a claim, as T-060 was on 29 September while unverified, by the rubric's anchor, movement on a central open case. $n = 17$ is, with $n = 12$ , one of the two open cases below $n = 18$ ; it is the case this project's own lane has worked longest, and the one the owner gave priority on 12 October. The claim settles it exactly at Bidwell's 1998 side, closing the whole 0.01508734360455 gap between the verified floor 4.66044275 and the certified ceiling, where T-093's step was 2.75e-6. The method composes this project's charge and local-isolation recipes with Ahmed's proof shape; that lineage is the credit line's business, not the score's. Significance is separate from whether this candidate proof is correct.
Composition: One cited entry, the source's report, which claims the exact value and carries the review of 12 October as its external_review; the lower half sets both rungs. The upper half, a packing at side L, is the certified endpoint T-065 holds (E-n017-certified-endpoint), V3/C3 here and independent of the source; the statement's F, G, rectangle and side map are that chart, which E-n017-overbeck-statement-root-independent decides again. Neither is cited, since citing the first would make this result hold the case's verified upper bound in T-065's place.

The lower half rests on five steps, and the capture step sets the minimum. Its 98 statements, 1,728,000 rows per checker, are the source's reported executions: 34 rows of 21 statements were reproduced with the producer's code (E-n017-overbeck-capture-sample-replay), 34 rows of six statements were decided again by an independent implementation (E-n017-overbeck-capture-independent-sample), and a sample decides no statement whole. Of the 13 trees, three were reproduced with the producer's code (E-n017-overbeck-tree-sample-replay) and ten were not run; one of the three, JQ, was also decided again by an independent implementation (E-n017-overbeck-jq-tree-review3), a sample of one tree.

The rigidity stage's finite rounds and contraction ran in the author's check.py (E-n017-overbeck-candidate-check-py-replay), which recomputes no capture row and no tree. These runs are evidence on the case record and are not cited here: each is a machine-shaped replay that passed on the part it ran, so citing them would make the checker derive a higher rung from parts, which this note would then have to set aside, as T-081's does; the case record cites them instead.

The second and third reviews' own programs decided, in full, the normalized 52-row gate (E-n017-overbeck-gate-review2), the root, the upper construction, the root admission, the literal facts of the capture step and the hand-overs (the E-n017-overbeck-*-review3 entries). Each decides a premise or a step other than the capture rows and the ten trees, so they too are on the case record and not cited here (epistemics.md, Every Run's Code Is Kept).

By epistemics.md's predicates: V3 needs, for every load-bearing part, a published or audited proof or a machine certificate whose replay passed, and the capture step and ten trees have neither, since a partial replay of the producer's computation is not a full replay and the source calls its proof a candidate. No numerical method (V1) or unavailable proof (V2) fits, so the result stands at V0. C3 would need confirming-origin machine evidence with a passing replay for every load-bearing part, and the same parts lack it; C2 needs a method that yields no certificate, which this is not. C1's predicate holds: a qualifying, dated read with its reviewer and note.
Next rung: V3 and C3 need every load-bearing part replayed in full, here or by a third party whose replay is retained here, the first review's section 5: the author's check.py to PASS, done on 12 October; all 98 capture statements, every row, with at least one of the producer's two capture checkers, compared row for row with the stored receipts; all 13 trees with at least one frozen checker and h_report30.py, three of them done; and one mutated-input control per kind, refused. That would be reproduction with the producer's code. An independent implementation of the capture sweep, begun on 34 rows, and of the tree checker, begun on the one-node tree JQ, would be an attribute beside the rung and not a rung.

V4 and C4 need, on top of V3 and C3, the owner's oversight record naming trust-boundary, certificate-meaning and ai-findings. The adversarial AI reviews they also need are on file: three, by distinct, separately prompted reviewers, all accepting, the second of which read the normalized 52-row gate of G20S_PHYSICAL (PROOF.md P110) and re-derived it with its own code. Their findings, ten, nine and seven, none blocking, are for the oversight record to disposition. Rung 5 needs the Lean formalization the source plans and has not started. T-154's Lean proof is separate: it proves the same equality by another route and does not formalize this argument.

On 13 October the owner held the ten-tree replay and the capture recomputation. Each remaining option, with its price and where it could run, is a bead under think-lqtu.
Unfinished confirmations: C3 (think-0at1): all 98 capture statements recomputed in full with the producer's capture checkers, 1,728,000 rows each, compared row for row with the stored receipts, with a mutated-certificate control refused: one of the two unfinished parts of C3, which T-153 reaches only when the ten-tree replay below has passed too, so this item stays listed until both have. About 1273 CPU-hours, up to about 2347 (priced 2026-10-12).

C3 (think-fgmr): the ten trees not yet replayed (JG, JPA_v5, G20S, HW, JPG15m_v5, JPG17p_v5, JPG3m_v5, JPG3p_v5, JPW13 and JPWS_v4) with the producer's two v3.0 checkers and h_report30.py, each report compared with the stored second execution, with a mutated-certificate control refused: the other unfinished part of C3, which T-153 reaches only when the capture recomputation above has passed too, so this item stays listed until both have. About 7.1 CPU-hours, up to about 21 (priced 2026-10-12).
Novelty: previously-published Present in an identified source

The case

Case record

4.664.676

456

4.1235.123

\sqrt{n}

\sqrt{n} + 1

Proven

$4.66044$ $\leq s (17) \leq$ $4.675531$

exact

Citation record n-017

lowerGuzhou0806 after Overbeck et al. 2026, GitHub (confirmed T-093)

upperBidwell 1998, Squares in Squares (confirmed T-065)

Open

optimality

The case record

LowerUpper

Verified

\frac{18641771}{4000000}

4.67553009…

Reported4.67553009…4.67553009…

Gap0.01508734…

Results on the case

19 results in the register on $n = 17$ , oldest first, each with what it established and how it stands now.

2005 published T-007
$s (n) \geq min (⌈ \sqrt{n} ⌉, \sqrt{n - 2 ⌊ \sqrt{n} ⌋ + 1} + 1)$ for $4 \leq n \leq 324$
V0 C1 Lower bound incomplete on this case, superseded by T-093 and T-153 (reported)
Nagamochi · Nagamochi 2005 · source · register
2026-08-21 published T-015
$s (17) \geq 22529 / 5000 = 4.5058$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Massaccesi after Burns · Burns–Massaccesi n17 · packet · register
2026-08-31 established T-001
$s (17) \geq 4426213 / 1000000 = 4.426213$ , from a sixteen-point unavoidable set
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Levy after Bentz · register
2026-08-31 established T-003
The sixteen-point set's unavoidability ceiling lies in $[4426213 / 1000000, 4427 / 1000)$
V3 C3 Method limit confirmed
Levy after Bentz · register
2026-09-04 established T-019
$s (n) \geq 459 / 100 = 4.59$ for $n = 17, 18, 19$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Levy after Burns, Massaccesi · register
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with $a > 3$ and $b > 2$
V3 C3 Correction confirmed
Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-20 published T-032
$s (17) \geq 461300 / 99999 = 4.61304613 \dots$ , and beneath it Mira's $s (17) \geq 4613 / 1000$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Guzhou0806, Mira-acc after Levy, Burns, Massaccesi · n17 weighted certificates 2026-09-20 · packet · register
2026-09-21 published T-038
$s (17) > 461300 / 99853 = 4.6197910929 \dots$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Overbeck after Levy, Mira-acc, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register
2026-09-21 published T-065
$s (17) \leq 4.6755300936045509 \dots$ , Bidwell's packing certified exactly
V3 C3 Upper bound confirmed
Overbeck after Levy, Mira-acc, Guzhou0806 · Kleddamag n17 certified bound · packet · source · review · register
2026-09-25 published T-039
$s (17) > 231001 / 50000 = 4.62002$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Guzhou0806 after Overbeck, Mira-acc, Levy · Guzhou0806 n17 R052 · packet · source · review · register
2026-09-26 published T-040
$s (17) > 232001 / 50000 = 4.64002$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Overbeck after Levy, Mira-acc, Guzhou0806 · Kleddamag n17 4.640020 · packet · source · review · register
2026-09-27 published T-041
$s (17) > 466001 / 100000 = 4.66001$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Overbeck after Levy, Mira-acc, Guzhou0806 · Kleddamag n17 4.66001 · packet · source · review · register
2026-09-28 published T-042
$s (17) > 233009 / 50000 = 4.66018$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Guzhou0806 after Overbeck, Mira-acc, Levy · Guzhou0806 n17 R067 · packet · source · review · register
2026-09-28 published T-043
$s (17) > 116511 / 25000 = 4.66044$
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Guzhou0806 after Overbeck, Mira-acc, Levy · Guzhou0806 n17 R068 · packet · source · review · register
2026-09-29 published T-058
Rectangle-certificate ceiling α·UB(n) proved for $n = 1$ ..100; B·UB(n) on 64 grid rows
V3 C3 Method limit confirmed
Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
$s (n) \geq 1 / 2 + \sqrt{n - ⌊ \sqrt{n} ⌋ + 1 / 4}$ for every nonsquare $8 \leq n \leq 324$
V3 C3 Lower bound confirmed on this case, superseded by T-093 and T-153 (reported)
Karakuş · Karakuş 2026 · source · register
2026-09-30 published T-093
$s (17) > 18641771 / 4000000 = 4.66044275$
V3 C3 Lower bound confirmed
Guzhou0806 after Overbeck, Mira-acc, Levy · Guzhou0806 n17 R071 · packet · source · review · register
2026-10-12 published T-153 this result
Candidate proof that Bidwell's 1998 packing is optimal, $s (17) = 4.67553009360455 \dots$
V0 C1 Optimality reviewed
Overbeck after Levy, Ahmed, Mira-acc, Guzhou0806, Maaz · Overbeck n17 candidate 2026 · packet · register
2026-10-12 published T-154
Fitzharding reports a Lean proof that $s (17) = 4.67553009360455 \dots$
V3 C1 Formalization reviewed
Fitzharding after Levy, Ahmed, MacIver · Fitzharding n17 Lean 2026 · packet · source · source build receipt · review 1 · review 2 · register

Links

On this site: Case record, $n = 17$ · Frontier row, $n = 17$ · T-153 in the results table

On GitHub, at main

Register: T-153 in results.yaml, line 17618
Evidence: E-n017-overbeck-optimality-candidate-report
Sources: Overbeck n17 candidate 2026 (its own site, retained copy)
Source packet: resources/web/kleddamag-n17-candidate-2026-10-12/README.md
Artifacts: 10 artifacts and controls
resources/web/kleddamag-n17-candidate-2026-10-12/README.md resources/web/kleddamag-n17-candidate-2026-10-12/facts/statement.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts/statement-comparison.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts/check-py/stdout.txt resources/web/kleddamag-n17-candidate-2026-10-12/receipts/recomputation-price.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts-here/upper-bound.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts-here/capture-sample.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts-here/capture-independent.json resources/web/kleddamag-n17-candidate-2026-10-12/receipts-here/trees.json docs/project/reviews/review-2026-10-12-kleddamag-n17-candidate.md
Case file: frontier/n-017.md (verified lower, verified upper, reported lower, reported upper)

T-153: Candidate proof that Bidwell's 1998 packing is optimal, s(17)=4.67553009360455…s(17)=4.67553009360455…

The case

Results on the case

Links

T-153: Candidate proof that Bidwell's 1998 packing is optimal, $s (17) = 4.67553009360455 \dots$