$n=17$$n=17$

$s(17)$$s(17)$ — open

$s(17)\le 4.6755300936045509516342148538535054$$s(17)\le 4.6755300936045509516342148538535054$ is now certified by exact identities and rational interval bounds. The reported record, $4.67553009360455\dots$$4.67553009360455\dots$, was found by Bidwell in 1998, building on a packing of Hämäläinen’s from 1980. The certified packing’s side is exactly that record: it is the root of the catalogue’s degree-18 polynomial, which is irreducible over $\mathbb{Q}$$\mathbb{Q}$ (exp-245; until 2 October 2026 this page recorded that identity as unproved), and the decimal above is a rational outward ceiling on it. The verified lower bound is the strict inequality $s(17)>18641771/4000000=4.66044275$$s(17)>18641771/4000000=4.66044275$, from Guzhou0806 / N17 project’s R071 release, published on 30 September 2026 and replayed here on 5 October, $11/4000000$$11/4000000$ above R068’s $116511/25000$$116511/25000$, whose charge it keeps. R071 keeps every point orbit, rule orbit and weight of R068 and rebuilds every strict core over $5,114$$5,114$ orientation intervals, with parents of side $18452000/18641771$$18452000/18641771$ in the same container $4613/1000$$4613/1000$. The budget stays $17000448944$$17000448944$ units of 10−9${10}^{-9}$, and the counting surplus stays $17\times 1000026844-17000448944=7404$$17\times 1000026844-17000448944=7404$. The package credits Overbeck for the $4.66001$$4.66001$ framework, proof and BigInt checker, and discloses AI assistance; its publisher checked file identities and saved records only, its row-level records are missing, and its CI replay passed unobserved, so the replay here is its first independent check. Both of its checkers ran here over every interval, Guzhou0806’s own C++ checker and Overbeck’s Node BigInt checker, the bytes R068’s replay here ran, and agree with each other on every interval minimum and cell count, every row at $1000026844$$1000026844$; both refuse two mutated certificates. This supports V3/C3 on one machine method: the two sweeps are one event-cell method, and this repository’s native parent-core route models only $k$$k$-of-$m$$m$ threshold atoms, so it cannot yet read the weighted and winning-subset features and gives no method-distinct decision. The proof review found no mathematical defect, re-derived every premise the new parent side and cores touch, and reproduced 227 rows of the replay’s ledger with a sweep sharing no code with the source; the two steps the source’s proof asserts are proved in the review of R067 and R068, and neither uses the parent side. R070’s obstruction shows this charge cannot prove a bound $1/40000000$$1/40000000$ higher, so a further step needs a new charge. The gap to the catalogue’s printed record is $0.01508734360455$$0.01508734360455$.

On 12 October 2026 Overbeck (GitHub Kleddamag) published a verification edition of a candidate proof that Bidwell’s packing is optimal, $s(17)=L$$s(17)=L$ (T-153; retained packet). Its statement defines $L$$L$ by this repository’s own H-255 chart: the same polynomials, the same isolating box of half-width 10−12${10}^{-12}$ and the same side map (6+4t)/(1+2t−t2)$(6+4t)/(1+2t-t^2)$, so its upper half is the certified endpoint above. The source calls it a “candidate proof, not an established theorem”, conditional on 210 listed obligations, 15 of them mathematical premises, in five steps: the upper bound; capture at side at most 4675531/106$4675531/{10}^6$ by 98 weighted counting certificates, leaving 11 cases; admission of each case into one of 11 regions; 13 tree certificates decided by two exact checkers; and a rigidity step that ends in a contraction of ratio $159201934153319/200000000000000$$159201934153319/200000000000000$. Its README says the mathematics, the engines, the certificates, the checkers, the reviews and the text were produced by AI systems under his direction, Codex (OpenAI) and Claude (Anthropic), and that within the project no human has read the mathematics; Guzhou0806 ran a checker of his own on two of the thirteen trees. The review of 12 October re-derived every hand step it could isolate and found no mathematical defect in what it read; it did not read the normalized 52-row gate of the rigidity step. The review of 13 October read that gate, re-derived it with its own code and found no blocking defect; it moves no rung. A third, mathematical-correctness review, written for the author, found no step false and no blocking defect; with code of its own it decided the root, the upper construction with every contact, the literal facts of the capture step, the admission of the eleven roots and the hand-overs, and the tree JQ, one of the thirteen, by a checker written from the specification. It moves no rung either. Here the author’s check.py passed, which recomputes no capture row and no tree; 34 capture rows of 21 statements and three of the trees were reproduced with the producer’s code, 34 rows of six statements were decided again by a checker written here from the proof text, and the root was isolated independently, all agreeing with the source. The complete capture recomputation (about 1,273 CPU-hours with the Python checker, the one C3 needs, and 2,347 with both checkers, by the source’s records) and ten trees have not been run, so the claim holds the reported lane, and the verified bounds and the status are unchanged.

Later the same day Fitzharding (GitHub ofitzharding) published a Lean 4 proof of the same equality using a different argument from Overbeck’s candidate, sq17-lean (T-154; retained packet), and asked for its registration in issue #565. Its theorem Sq17.square17_optimality states that seventeen closed unit squares, each independently translated and rotated, with disjoint interiors, fit in [0,L]2$[0,L{]}^2$ exactly when $L$$L$ is at least EndpointGeometry.side, which is this case’s $L$$L$ by identity of definition: the same H-255 polynomials, the same isolating box and the same side map. The theorem justifies certificate acceptance and every case exclusion. Its trust boundary is Lean’s kernel for the geometric arguments and Lean’s compiler, native evaluator and C toolchain for 13,343 native_decide facts. The proof runs on this project’s $n=17$$n=17$ plan and data: exp-247’s 24-cell cover, the census, 32 patterns of the certified sub-pattern ledger, the endpoint chart and the 52-row local recipe, which its README credits only as the project’s “wider research record”. What it adds is the exclusion of every residual case, the capture, and a Lean proof of each bridge from a certificate to geometry. Its README says the project “was developed with substantial assistance from Claude and Codex”, and the author’s post says it was “Built with @OpenAI Astra + @AnthropicAI Opus 5.5”. The review of 13 October read the statement, the endpoint and the trust boundary and found no mathematical defect, and a second, mathematical-correctness review, written for the author, read the checkers and their soundness proofs and found none either. With code of its own it recomputed the census, the interior cells’ capacities and the 93-box dual certificate exactly and re-evaluated ten of the 13,343 native_decide facts, a sample, all agreeing; neither review built the proof, and neither moves a rung. The owner classified this as a formalization on 13 October 2026: it proves the recorded value and is the first proof-assistant proof in this record. T-153’s release was public about six hours before this proof’s repository, and T-153 keeps the reported lower bound. The source reports a clean rebuild of the theorem’s 4,951-module import closure on the author’s machines, and an audit of its retained receipt admits that build as source verification; nothing here has built it, so the verified bounds and the status are unchanged.

The previous verified lower bound was $116511/25000=4.66044$$116511/25000=4.66044$, from Guzhou0806 / N17 project’s R068 release, published on 28 September 2026 and replayed here that night, $43/100000$$43/100000$ above Overbeck’s $4.66001$$4.66001$, whose charge it continues. R068 keeps that charge’s $889$$889$ rule orbits and their weights unchanged, moves one zero-weight site orbit by $1/12500$$1/12500$, adds one weighted four-site point orbit on the diagonal at $(1.34,1.34)$$(1.34,1.34)$, and rebuilds the strict cores over $4,991$$4,991$ orientation intervals, with parents of side $115325/116511$$115325/116511$. Its two checkers, the same as R071’s, ran here over every interval and agree with each other and with the published ledgers. The same day’s R067, $233009/50000=4.66018$$233009/50000=4.66018$, ran the $4.66001$$4.66001$ charge unchanged at parent side $32950/33287$$32950/33287$ over $2,808$$2,808$ intervals; it was replayed here in full too and never held the verified field. R070 of 29 September, $46604427/10000000=4.6604427$$46604427/10000000=4.6604427$ over $5,107$$5,107$ intervals, is the release R071 refines; it was never replayed here and never held the verified field.

Before R068 the verified lower bound was $466001/100000=4.66001$$466001/100000=4.66001$, published on 27 September 2026 and replayed here the same day. Overbeck, building on Squares Project (Levy), Mira and Guzhou0806: an exact weighted-certificate proof over 2,168 orientation intervals. That is the lineage the release’s own ATTRIBUTION.md states — this project’s weighted-covering, strict-core, event-cell and threshold-budget methods, Mira’s 17squares support and parent-angle catalogue, and R038’s parent-side reduction — and the release claims no invention of those methods and says that attribution implies no upstream coauthorship or endorsement. Its AUTHORS.md names Overbeck as Kleddamag and says the work was produced with AI agents (OpenAI Codex) under his direction. It keeps Overbeck’s parent-core architecture — container side $4613/1000$$4613/1000$, here with parents of side $461300/466001$$461300/466001$ — and combines two completed charge candidates: $224$$224$ point orbits, $225$$225$ two-of-three, $30$$30$ three-of-five and two four-of-seven threshold orbits, $154$$154$ weighted-threshold orbits in four coefficient patterns and $254$$254$ pairwise-intersecting winning-subset orbits on three to ten sites, $7,048$$7,048$ feature images in all over $2,620$$2,620$ site orbits ($20,856$$20,856$ sites). Every one of its $86$$86$ distinct rules has capacity one. Both of the source’s complete checkers, a Python sweep in rational arithmetic and a JavaScript BigInt sweep, are the v1.1.0 engines byte for byte; they ran here over every interval and agree on every interval minimum and cell count. The counting surplus is $17\times 1000026844-17000402008=54340$$17\times 1000026844-17000402008=54340$ units of 10−9${10}^{-9}$. This supports V3/C3 on one machine method: the two sweeps are one event-cell method, and this repository’s native parent-core route models only $k$$k$-of-$m$$m$ threshold atoms, so it cannot yet read the weighted and winning-subset features and gives no method-distinct decision. The proof review is a separate record, docs/project/reviews/review-2026-09-27-n17-kleddamag-466001.md. R068 exceeds it by exactly $43/100000=0.00043$$43/100000=0.00043$.

Before that the verified lower bound was $232001/50000=4.64002$$232001/50000=4.64002$, from Overbeck’s v1.1.0 release of 26 September 2026, replayed here on 27 September: Overbeck, building on Squares Project (Levy), Mira and Guzhou0806, on the same lineage. It widened Overbeck’s own v1.0.0 charge dictionary to $280$$280$ point orbits, $155$$155$ two-of-three, $26$$26$ three-of-five and one four-of-seven threshold orbit, $54$$54$ weighted-threshold orbits (coefficients $2,1,1,1$$2,1,1,1$, threshold $3$$3$) and $30$$30$ pairwise-intersecting winning-subset orbits over $2,048$$2,048$ angle intervals, with parents of side $32950/33143$$32950/33143$ and a counting surplus of $17\times 998727933-16978369232=5629$$17\times 998727933-16978369232=5629$ units of 10−9${10}^{-9}$, also at V3/C3. Its review found no mathematical defect. Its AUTHORS.md names Overbeck as Kleddamag and says he directed the work and that separate OpenAI Codex research tasks constructed and exactly checked the $4.640020$$4.640020$ certificate. The $4.66001$$4.66001$ bound exceeds it by exactly $1999/100000=0.01999$$1999/100000=0.01999$.

Before v1.1.0 the verified bound was $231001/50000=4.62002$$231001/50000=4.62002$, from the R052 release of Guzhou0806 / N17 project, published on 25 September 2026 and replayed and reviewed here the same day. R052 was produced with AI assistance on Overbeck’s v1.0.0 mixed point/threshold parent-core architecture and extends Guzhou0806’s own R050 with enlarged resources: $2,354$$2,354$ point orbits and $514$$514$ two-of-three and $54$$54$ three-of-five threshold orbits ($18,585$$18,585$ sites, $4,504$$4,504$ groups, $2,922$$2,922$ columns) over $15,721$$15,721$ angle intervals. Its SOURCE_NOTICES.md says Guzhou0806 / N17 project used AI assistance for exploration, implementation, computation, checking and documentation, with non-proposer AI review in its final local acceptance, and names Mira-acc/17squares and Levy’s squares project in its method lineage. The source’s Python/Numba and Node/BigInt sweeps both ran here over every interval, and each reproduced the source’s own row ledger byte for byte. The counting surplus is $17\times 999426274093-16990246659579=2$$17\times 999426274093-16990246659579=2$ units of 10−12${10}^{-12}$, no slack beyond integer rounding. That too is V3/C3 on one machine method: the native interval route verifies every exact premise but refuses the coverage at its engine ceilings. Its review found no mathematical defect. Overbeck’s v1.1.0 exceeds it by exactly $1/50=0.02$$1/50=0.02$.

Before R052 the verified bound was $461300/99853=4.619791092907\dots$$461300/99853=4.619791092907\dots$, from Overbeck’s v1.0.0 release, replayed and reviewed here on 21 September 2026. Its complete Python and JavaScript scans cover all $7,853$$7,853$ parent-angle intervals, agree on all $509$$509$ histogram bins, and give $17\times 1000020517-16998427356=1921433$$17\times 1000020517-16998427356=1921433$ integer units of counting surplus, also at V3/C3. R052 exceeds it by $1142853/4992650000\approx 0.000229$$1142853/4992650000\approx 0.000229$. Its AUTHORS.md names Overbeck as Kleddamag and says he initiated and directed the project and OpenAI Codex performed the mathematical exploration, the searches and checks, and the certificate and proof. Before that, the verified bound was $461300/99999=4.61304613\dots$$461300/99999=4.61304613\dots$, from Guzhou0806’s R012 parent-angle certificate of 20 September 2026 (T-032), which remains valid historical evidence at V3/C3, confirmed by two machine methods: the source’s own checker re-run, and an independent re-implementation here.

R012 uses this repository’s weighted method with three changes and was the first external certificate to supply this case’s verified bound. Instead of covering every closed $B$$B$-square, it covers only what a real parent needs: squares of side $A=99999/100000$$A=99999/100000$ inside [0,4613/1000]2$[0,4613/1000{]}^2$, with the bound $L/A$$L/A$ recovered by rescaling at the end. A catalogue of $2925$$2925$ closed parent-angle intervals covers $[0,\pi /4]$$[0,\pi /4]$, and each interval chooses its own concentric closed core — its own direction and its own side — strictly inside every parent of that interval. Coverage is then required only over the legal parent-centre square for the interval, which is smaller than the set of all contained cores, and that restriction is what the extra strength buys: five placements the source retains as counterexamples fail the unrestricted test and pass this one. The measure is $1616$$1616$ atoms in $206$$206$ D4 orbits of total mass $424969/25000$$424969/25000$, every core captures at least $\gamma =250023/250000$$\gamma =250023/250000$, and $17\gamma$$17\gamma$ exceeds the mass by $701/250000$$701/250000$. It is decided at V3/C3 by two methods that fail differently: the source’s own exact event-cell checker, which recomputed all $2925$$2925$ intervals here over $9,231,165$$9,231,165$ centre strips, and this repository’s interval branch and bound, which certified the same $2925$$2925$ entries over $34,465,227$$34,465,227$ boxes with none stalled and every bracket containing the exact minimum. The catalogue minimum is exactly $\gamma$$\gamma$, so there is no slack anywhere: raising the threshold by one part in 106${10}^6$ at an entry that attains it is refused.

Beneath it sits the certificate R012 is built on, which was the strongest value on record until R012 passed it thirteen days later. Mira’s weighted certificate of 7 September 2026 gives $s(17)\ge 4613/1000=4.613$$s(17)\ge 4613/1000=4.613$ on $1620$$1620$ atoms of mass $849899249/50000000$$849899249/50000000$, core side $19997/20000$$19997/20000$ and a $2880$$2880$-step direction net, with least covered mass $1000002103/1000000000$$1000002103/1000000000$. It is written in this repository’s own certificate schema — it starts from the T-019 atoms and retains that file unchanged — so both stock verifiers decide it with no translation layer, and both accept it: the exact sweep finds that least value at net direction $2194$$2194$, and the interval route pins it on the doubled $5761$$5761$-direction net to a zero-width enclosure at the same rational. Mira’s own headline is larger, the dilation endpoint $4.61302863588611\dots$$4.61302863588611\dots$, but that step needs a T-022-style proof note this certificate does not carry, so the record holds the container side. Nothing is lost: R012’s value is larger still.

Both results descend from this repository’s T-019 and credit it, and both disclose model assistance and claim neither peer review nor priority. R012’s ATTRIBUTION.md names it as research by “Guzhou0806 / N17 project, with AI assistance”, and Mira’s paper says its earlier computation and exposition “were developed with assistance from OpenAI’s GPT-5.6 Pro under human direction” and that the September patch and its integration also used AI assistance. Mira’s certificate was published hours after the 7 September GitHub check that built the earlier packet, which is why neither was in the record until 20 September. The two are separate results with separate premises: R012 recomputes every obligation on its own measure and does not depend on Mira’s certificate being valid. What the machines do not decide is the reduction from a packing to R012’s $2925$$2925$ finite obligations — the angle folding, the endpoint containment test, the union of centre squares, the counting and the rescaling. Those were read line by line in the proof review, which found no error and supplied two steps the source’s note omits.

Weaker bounds are kept for their provenance rather than their strength. This repository’s own T-019, $s(17)\ge 459/100=4.59$$s(17)\ge 459/100=4.59$ of 2026-09-04, held the case until R012 displaced it: 1184 rationally weighted atoms of total mass $423327/25000$$423327/25000$, least covered mass $200009/200000$$200009/200000$, decided by the same two verifiers. It is still the ancestor of everything above it, and it still holds $n=18$$n=18$ and $n=19$$n=19$ in company with the certificates that have since passed it there. Massaccesi’s August 2026 certificate ([Burns–Massaccesi n17], T-015) gave $22529/5000=4.5058$$22529/5000=4.5058$ — 168 rationally weighted atoms of total mass $203/12<17$$203/12<17$, reduced exactly to 181 rational directions and $16,562,293$$16,562,293$ event cells — and held this case from 2026-09-03 until T-019 displaced it a day later. It is source-backed, from a blog post by Massaccesi, who marks the value “(?)”; it is replayed here twice, by the retained source verifier and by an accumulation-independent repository instrument that agrees on every direction cell (H-052, exp-059), with the argument audited lemma by lemma (BC-150 packet, BC-151 review). It is also the control that tests this repository’s verifiers rather than its certificates, and it still is. Massaccesi’s certificate re-parametrises Burns’s note of 6 August 2026, which proposed the side $44811/10000=4.4811$$44811/10000=4.4811$ on 268 atoms of total mass $16.9476$$16.9476$ with least covered mass $10003/10000$$10003/10000$, and whose verifier is the one Massaccesi modified; that verifier replays here unchanged (E-n017-burns-source-replay, 7 September 2026), the repository’s exact sweep accepts the same atoms re-encoded as a control (E-n017-burns-control-decision, a published control whose least covered mass is not exactly $1$$1$), and its rung sat between Brandwijk’s $89/20$$89/20$ capsule of 18 July and Massaccesi’s value for a fortnight. The note’s byline is “ChatGPT (GPT-5.6 Pro, OpenAI)”; Burns’s post says the model “developed the certificate during this project” and that he operated it. Burns’s companion post describes a near-record arrangement at side $4.677648$$4.677648$, $0.002118$$0.002118$ above Bidwell’s, with eleven axis-aligned squares and six at a common tilt of 39.6319∘${39.6319}^{\circ }$, a contact topology he reports as distinct from Bidwell’s; the coordinates are retained under resources/web/burns-n17-series-addendum-2026-09-07/, and the contact graph has not been reconstructed here. Below it, the repository’s own sixteen-point certificate — cases/green17, $s(17)\ge 4.426213$$s(17)\ge 4.426213$, T-001, certified by the Bentz-lemma cell certificate and an independent interval branch-and-bound — was previously the second strongest and remains a first-party theorem confirmed by two methods, its producer’s code re-run and an independently re-implemented interval audit, above Nagamochi’s general $4.162278$$4.162278$ and a hair below Green’s reported but sourceless (402​+19)/17≈4.4452$(40\sqrt{2}+19)/17\approx 4.4452$. Certifying the sixteen-point set at its exact ceiling 753/250+2​≈4.42621356$753/250+\sqrt{2}\approx 4.42621356$ is a typed follow-on (think-iye2). Green’s own sixteen points, which DS7’s Figure 34 calls unavoidable at his value, are not: a closed unit square in the container misses all of them by $0.00545$$0.00545$, so the figure proves no bound above about $4.3978$$4.3978$ (review). An earlier audit catalogued eight public lower-bound postings for this size between 18 July and 21 August 2026, and the record’s indexed corpus held three of them. Kim Brandwijk’s Zenodo capsule of 18 July gave $89/20=4.45$$89/20=4.45$ from an exact sixteen-point set; Burns’s note of 6 August gave $44811/10000=4.4811$$44811/10000=4.4811$. Three GitHub repositories followed, none of them in the indexed corpus until the 7 September 2026 check that found them ([GitHub n17 certificates 2026]): Mira’s first version on 10 August at $4.450837$$4.450837$, Stanislav Fort’s on 11 August at $4.456575$$4.456575$, and Mira’s second on 11 August at $4.468292$$4.468292$. Those three are exact sixteen-point certificates on one architecture — the pose space subdivided in integer arithmetic into point, piercing and infeasible leaves — and they are the strongest integral sixteen-point bounds on record, above both Brandwijk’s capsule and cases/green17; Mira’s and Fort’s replay here under their own Python checkers (E-n017-mira-point-certificate-replay, E-n017-fort-point-certificate-replay). anabologyco-maker’s repository followed with $4.57$$4.57$ on 13 August and the side $9141/2000=4.5705$$9141/2000=4.5705$ on 16 August: 560 weighted atoms on the $1/4000$$1/4000$ grid, decided not over a direction net but over an exact orientation partition of $148,937$$148,937$ cells, with a Lean 4 layer over the finite checks. It is source-backed only — its decisive Sturm, endpoint and coverage stages need Boost and its Lean layer needs Lean 4.33, neither available here (E-n017-anabologyco-weighted-certificate) — and it was the strongest public value on record until Mira’s certificate of 7 September passed it. Massaccesi’s $22529/5000$$22529/5000$ closed the sequence on 21 August. Corrected 2 October 2026: Nagamochi’s value is now a reported bound, his Lemma 1 being false (Karakuş 2026; review). This register had recorded that proof as verified, its own error, logged as defect D-516.

Later public claims improved on the historical R012 value $461300/99999$$461300/99999$.

Guzhou0806’s R038 certificate, in the same repository, reports the strict lower bound $461300000000/99974999999=4.614153538431\dots$$461300000000/99974999999=4.614153538431\dots$. Its complete published proof, checker, source pin and source-result files are now retained in the Guzhou source tree. That release keeps its required Mira numerical certificate external, identified by SOURCE_PIN.json; retaining the tree does not replay the geometric obligations. No local complete R038 replay is claimed, and the verified field does not rely on it.

Overbeck’s $461300/99853=4.619791092907\dots$$461300/99853=4.619791092907\dots$, the v1.0.0 release, was the verified bound from 22 to 25 September 2026 and is now the previous one. Its bytes are retained here, a full two-checker replay reproduced its published RESULT.json byte for byte, and the review found no blocking defect. The verified field recorded that result through E-n017-kleddamag-461300-99853-source-replay, which remains valid evidence. The decision before 22 September to wait for a method-distinct checker was an admission-policy error: the complete rigorous replay and discharged proof assumptions already supported a verified bound at C3. The replay date remains 21 September; no new full replay was run for that record correction on 22 September.

The packet retains the source’s manifest-bound result bytes, and Session 150 and the review attest that the local run reproduced them. A separately named local raw replay directory was not retained; the source outputs are not relabelled as local receipts. T-032 keeps its original R012 statement and evidence; adopting the stronger external bound neither rewrites that result nor creates a new theorem identifier.

Guzhou0806 then published three releases on Overbeck’s architecture, each numerically superseded by R052 and each retained here only as a publication record in the R052 packet, none replayed: R042 on 23 September ($115325/24963\approx 4.619837$$115325/24963\approx 4.619837$), R043 the same day ($461300/99851\approx 4.619884$$461300/99851\approx 4.619884$), and R050 on 24 September ($4613000/998509\approx 4.619888$$4613000/998509\approx 4.619888$). R052’s geometry is R050’s, uniformly rescaled, with five of R050’s $15,706$$15,706$ angle rows each split into four. The complete R052 package, its four replay receipts and the native route’s refusal are retained here, and the verified field records the result through E-n017-guzhou-r052-source-replay. As with Overbeck’s bound, no new theorem identifier is created. Deciding the certificate natively needs the interval engine’s atom, site and member-slot ceilings raised in a new proof commit; a sizing run on four of its rows prices the full run at roughly 8 to 49 CPU-hours, an estimate and not a decision.

Overbeck’s v1.1.0 release of 26 September 2026 then raised the bound to $232001/50000=4.640020$$232001/50000=4.640020$. Its new package, bounds/4.640020/, carries the certificate, a proof and method note, a general-rule Python checker and a separately written JavaScript BigInt checker, a controls script, and the source’s own receipts; the v1.0.0 files are unchanged in the same tree. The release measures its advance against its own $4.619791\dots$$4.619791\dots$, not against R052, and states that no code from R052 was used. The packet retains every file that changed or was added since v1.0.0, and the verified field records the result through E-n017-kleddamag-4640020-source-replay. As with the earlier external bounds, no new theorem identifier is created. Its budget rules go beyond the architecture reviewed on 21 and 25 September: a weighted threshold charges at most ⌊Σai​/k⌋$\lfloor \Sigma a_i/k\rfloor$ disjoint cores, and a winning-subset feature whose listed subsets pairwise intersect charges at most one. Deciding it natively needs the parent-core route to represent both feature kinds before any coverage engine question arises.

A later revision of the same repository, of 27 September 2026 and not yet tagged (its changelog lists it as unreleased), then raised the bound to $466001/100000=4.66001$$466001/100000=4.66001$ in a new package, bounds/4.66001/. Its checkers and their shared modules are the $4.640020$$4.640020$ bytes; only the launcher’s target and interval count and the controls’ target and sampled intervals change. The certificate combines completed charges from two separate research tasks and subdivides eight of an original $2,048$$2,048$ intervals sixteen ways with regenerated strict cores, keeping the charge fixed. Its embedded source string still reads “exact diagnostic pending”, which the release explains as preserved text from an earlier construction stage, kept so that the certificate file is unchanged. The packet retains every file that changed or was added since v1.1.0, and the verified field records the result through E-n017-kleddamag-466001-source-replay. No new theorem identifier is created. The feature kinds and budget rules are the ones v1.1.0 introduced, on many more orbits: the weighted thresholds now include coefficients $2,1,1,1,1,1$$2,1,1,1,1,1$ at $4$$4$, $2,1,1,1,1,1,1,1$$2,1,1,1,1,1,1,1$ at $5$$5$ and $4,1,1,1,1,1$$4,1,1,1,1,1$ at $5$$5$, each still firing at most once on disjoint cores, and the winning-subset rules run on three to ten sites.

Guzhou0806 / N17 project’s R067 and R068 packages, published on 28 September, are retained with complete paired replays of both in their packet. The verified field recorded R068 through E-n017-guzhou-r068-source-replay from 29 September to 5 October, and R067, the intermediate, is recorded through E-n017-guzhou-r067-source-replay. As with the earlier external bounds, no new theorem identifier is created. R068 also ships the C010 research material: a shifted-core strip sweep and an exact counterexample to a separate charge aimed at $9321/2000$$9321/2000$, which the source says is not a global bound and which carries none here.

Guzhou0806 / N17 project’s R070 and R071, published on 29 and 30 September, are retained in their packet, with the complete paired replay of R071 here and its two mutated-certificate controls. The verified field records R071 through E-n017-guzhou-r071-source-replay; R070 has no entry and was not replayed. Both keep R068’s charge exactly — every point orbit, rule orbit and weight, the budget $17000448944$$17000448944$ and the requested minimum — and rebuild every strict core for a smaller parent. R070 claims $46604427/10000000=4.6604427$$46604427/10000000=4.6604427$ over $5,107$$5,107$ intervals that refine R068’s $4,991$$4,991$, and publishes complete four-partition C++ and BigInt ledgers, which agree row by row here: every interval at minimum $1000026844$$1000026844$, surplus $7404$$7404$. R071 is built on R070’s certificate, bisects seven of its intervals, and claims $18641771/4000000=4.66044275$$18641771/4000000=4.66044275$ over $5,114$$5,114$; its row-level records are missing, as the source says, and a completion summary of a three-partition run reports the same minimum and surplus and names the BigInt checker and launcher bytes R068’s replay here ran. The replay here regenerated both ledgers: the two agree on every row, every row at minimum $1000026844$$1000026844$, $2,263,809,819,494$$2,263,809,819,494$ cells in all. The source’s own GitHub Actions replays of both passed; their publisher, which discloses AI assistance, did not observe them. Neither release’s other material carries a bound: R070’s same-budget overlay of $319$$319$ orbits and its obstruction at one parent within a fixed-weight enhancement class, and R071’s conditional joint geometry at $9321/2000$$9321/2000$ inside one first-anchor box, which the source says does not prove $s(17)>4.6605$$s(17)>4.6605$.

Three other public reports are recorded without carrying a bound here. ahyangyi’s 17squares v1.1.1 of 23 September reports $184547267428061/40000000000000\approx 4.6136817$$184547267428061/40000000000000\approx 4.6136817$, below R038 and below the verified bound; its author’s commit message says it is not frontier any more, and it is not retained. Overbeck’s untagged v1.2.0 of 29 September reports $46601/10000=4.6601$$46601/10000=4.6601$, its $4.66001$$4.66001$ charge unchanged over $2,543$$2,543$ intervals, with a research checkpoint of conditional exclusions and unfinished routes that claims no bound; it is below R067 and below the verified bound, asks for no work, and is not retained. R052’s source also reports that Overbeck holds an unpublished internal strict bound of $4.62001$$4.62001$. That is second-hand, below R052 and unverified, and it is not recorded here as a bound.

Guzhou0806’s R052 continuation, published on 25 September, claims $s(17)>462003/100000=4.62003$$s(17)>462003/100000=4.62003$ from R052’s sites moved by an exact D4-symmetric deformation and two more angle rows split four ways ($15,727$$15,727$ rows, surplus again 2 units). Overbeck’s public $232001/50000=4.64002$$232001/50000=4.64002$ of 26 September supersedes it, so it is kept only as a publication record in its own packet, with local receipts for its records, containment and new C++ full replay. That C++ kernel runs the same exact event-cell sweep as the source’s Python and Node/BigInt checkers, so it is not a method-distinct decision.

An additional source, MacIver’s manuscript dated 8 August 2026, reports s(17)>(402​+19)/17+1/200≈4.450208382054341$s(17)>(40\sqrt{2}+19)/17+1/200\approx 4.450208382054341$ by deforming Green’s sixteen-point scaffold and using conditional counting. The archived source review retains the paper at its public 10 August commit, together with his center-area and center-count manuscripts. The n17 claim is historical and source-reported: the public Lean file proves supporting algebra, while the fourteen certificate files and exact ledger/assembly scripts needed for the full bound are absent from the inspected snapshot. The operative verified lower bound is Guzhou0806’s strict R071 bound $18641771/4000000$$18641771/4000000$ described above; the MacIver claim remains historical and source-reported.

Certified Endpoint Upper Bound

The exact root and centroid construction certify 17 unit squares in a square of side at most $4.6755300936045509516342148538535054$$4.6755300936045509516342148538535054$. This is a rational outward ceiling, not a claim that the endpoint side equals that decimal. The endpoint review records all 68 wall and 136 pair obligations and an independent exact interval audit. It improves the earlier rational witness at 4675530093604551/1015$4675530093604551/{10}^{15}$, which remains a verified fallback.

The upper ceiling agrees with Bidwell’s catalogue decimal at its printed precision, and since 2 October 2026 the side is identified exactly. The chart polynomials’ resultant has one irreducible degree-18 factor with a root at the certified point, and mapped to the side it is the catalogue’s polynomial with unit 1 (H-265, exp-245, output review). The certified side is therefore Bidwell’s algebraic number S∗$S^{*}$, and the decimal is a ceiling on it. Neither result proves a global minimum. The lower bound remains strictly below it, so status remains open.

The attempt to prove s(17)=S∗$s(17)=S^{*}$ follows the local half, global half and capture that settled $n=11$$n=11$. Each part and the evidential status of each claim are explained in The n = 17 Optimality Proof, Explained. None of it moves a bound or the status.

Three orientation classes, and a correction

This is the smallest case whose best known packing uses squares at three different angles, a distinction frequently misattributed to $n=11$$n=11$ (which uses two: axis-aligned and ≈40.182∘$\approx {40.182}^{\circ }$). Bidwell’s packing uses the unequal nonzero orientations +39.8049589798∘$+{39.8049589798}^{\circ }$ and −36.6237863834∘$-{36.6237863834}^{\circ }$, not the symmetric shorthand ±40∘$\pm {40}^{\circ }$ previously stored here. Those values are transcribed from the analytic entities in the primary Kingbird SVG. The certified endpoint is a separate exact reconstruction. Its side is the catalogue’s degree-18 root (exp-245); that its configuration is the pictured packing, contact for contact, has not been established.

Degree 18

The catalogue reports a side length algebraic of degree 18 — more than twice the degree at $n=11$$n=11$, and a useful calibration on how fast algebraic complexity grows once the contact graph stops being simple. Gensane and Ryckelynck derived it from a four-equation system of degree 7 in cosθ1​,cosθ2​,sinθ1​,sinθ2​$\cos {\theta }_1,\cos {\theta }_2,\sin {\theta }_1,\sin {\theta }_2$, and observed that Friedman’s rounded $4.6755$$4.6755$ “seems to be false.”

Their reported decimal and the catalogue’s differ from the ninth decimal onward ($4.6755300960455$$4.6755300960455$ versus $4.67553009360455$$4.67553009360455$). Direct evaluation resolves the numerical discrepancy in favour of the catalogue: the stored degree-18 polynomial has a root $4.6755300936045509516\dots$$4.6755300936045509516\dots$, within 9.52×10−16$9.52\times {10}^{-16}$ of the catalogue decimal, while the reported decimal is 2.44×10−9$2.44\times {10}^{-9}$ away and gives polynomial residual about $56.9$$56.9$. The remaining source question is whether the paper has a decimal transcription slip or intended a different equation. Since 2 October 2026 the certified endpoint’s side is identified with that root exactly (exp-245). The polynomial is irreducible over $\mathbb{Q}$$\mathbb{Q}$, by factorization and by Rabin tests at four primes in the independent review. S∗$S^{*}$ therefore has algebraic degree 18, with this polynomial as its minimal polynomial; the review encloses S∗=4.6755300936045509516341112704831466487671…$S^{*}=4.6755300936045509516341112704831466487671\dots$ to width 10−40${10}^{-40}$.

Why it matters downstream

$s(17)$$s(17)$ is a workhorse: the catalogue records several larger records — $s(83)$$s(83)$, $s(84)$$s(84)$, and others — as extensions of Bidwell’s packing. An error in it would propagate.

Reported Lower Bound

The reported lower bound is Overbeck’s candidate equality $s(17)=L=4.67553009360455095163\dots$$s(17)=L=4.67553009360455095163\dots$ (T-153, 12 October 2026), described above. Fitzharding’s Lean proof of the same equality, published later that day (T-154), is recorded as a formalization, a proof-assistant proof of the same value by a route of its own, and this lane stays on T-153, the first report. Before it the reported lower bound was Guzhou0806’s strict R071 bound $s(17)>18641771/4000000=4.66044275$$s(17)>18641771/4000000=4.66044275$, on R068’s continuation of Overbeck’s $4.66001$$4.66001$ charge (retained packet), which since its complete paired replay here on 5 October 2026 is the verified bound too. R068’s $116511/25000$$116511/25000$, R070’s $46604427/10000000$$46604427/10000000$, Overbeck’s $466001/100000$$466001/100000$, its v1.1.0 $232001/50000$$232001/50000$, Guzhou0806’s R052 $231001/50000$$231001/50000$, Overbeck’s $461300/99853$$461300/99853$, Guzhou0806’s earlier R012 result and R067 remain recorded above as historical evidence.

Verification Code

The programs behind this case’s verified bounds, by their evidence. The code column says how the code that ran stands to the code its producer used. VERIFIERS.md says what each program is and whose it is.