T-038:
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
= 4.6197910929..., by Overbeck's 17-squares-certified-bound v1.0.0 release of 21 September 2026. It raised the verified bound by 0.0067450 over Guzhou0806's R012 (T-032).
The certificate is a mixed point and two-of-three threshold charge, exact, nonnegative and D4-invariant, of budget 16998427356 integer units, over 7,853 contiguous parent-angle intervals, each with a closed core strictly inside every parent, in the container 4613/1000 with parents of side 99853/100000. The minimum core charge 1000020517 gives seventeen cores a surplus of 1921433 over the budget, and compactness makes the bound strict.
It was replayed here in full on 21 September 2026 by the source's two complete checkers, a Python and a JavaScript event-cell sweep, which agreed on all 509 histogram bins; they are one method.
Overbeck, 17-squares-certified-bound, in the lineage the release names itself: Mira, Guzhou0806 / N17 project, and this repository's threshold-atom work. Its AUTHORS.md names Overbeck as Kleddamag and says he directed the project, with the research, implementation and verification done by OpenAI Codex.
Significance, composition and next rung
- Significance
- Raised the verified lower bound at by 0.0067 over R012 and brought into the record the mixed point/threshold parent-core architecture every later rung is built on. S3 by the T-015 and T-032 precedent, read as the rubric reads it: a result by others takes the score its claim would take from anyone, and the replay here is confirmation, not significance. Confirmed on 11 October: the parent-core charge is the architecture of Overbeck's certificate (T-037) at a second count, a further size from one generator at S3 by T-020's calibration, beside T-032 at the same count.
- Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained. Unlike the later releases, this certificate carries only point and two-of-three atoms, which this repository's native parent-core route models, so a complete native run of it is the reachable second machine method, which would be shown beside the rung. No test under packing/tests exercises this packet; the control named is the release's own independent_controls.py, which the 2026-09-21 review used to close the containment and centre-domain premises. Rung 5 needs a proof-assistant formalization reviewed by human experts. Superseded as the verified lower bound on 2026-09-25 by Guzhou0806's R052 (T-039); stays true as stated.
- Novelty
- previously-published Present in an identified source
The case
Proven
- 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
Results on the case
19 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007
for
V0 C1 Lower bound incomplete on this case, superseded by T-093 and T-153 (reported)
2026-08-21 published T-015
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
, from a sixteen-point unavoidable set
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
2026-08-31 established T-003
The sixteen-point set's unavoidability ceiling lies in
V3 C3 Method limit confirmed
2026-09-04 established T-019
for
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 and
V3 C3 Correction confirmed
Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-20 published T-032
, and beneath it Mira's
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 this result
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
, 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
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
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
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
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
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 ..100;B·UB(n)on 64 grid rowsV3 C3 Method limit confirmed
Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
for every nonsquare
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
V3 C3 Lower bound confirmed
Guzhou0806 after Overbeck, Mira-acc, Levy · Guzhou0806 n17 R071 · packet · source · review · register
2026-10-12 published T-153
Candidate proof that Bidwell's 1998 packing is optimal,
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
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, · Frontier row, · T-038 in the results table
On GitHub, at main
- Register
- T-038 in
results.yaml, line 3408 - Evidence
E-n017-kleddamag-461300-99853-report·E-n017-kleddamag-461300-99853-source-replay- Proofs and certificates
- certificate
global-certificate.json· proofPROOF.md· auditreview-2026-09-21-n17-kleddamag-461300-99853.md - Sources
- Kleddamag n17 certified bound (its own site, retained copy)
- Source packet
resources/web/n17-kleddamag-certified-bound-2026-09-21/README.md- Artifacts
6 artifacts and controls
resources/web/n17-kleddamag-certified-bound-2026-09-21/README.mdresources/web/n17-kleddamag-certified-bound-2026-09-21/kleddamag-17-squares-certified-bound/PROOF.mdresources/web/n17-kleddamag-certified-bound-2026-09-21/kleddamag-17-squares-certified-bound/RESULT.jsoncampaign/agent-sessions/session-150-n17-consolidation-and-correctness.mddocs/project/reviews/review-2026-09-21-n17-kleddamag-461300-99853.mdresources/web/n17-kleddamag-certified-bound-2026-09-21/kleddamag-17-squares-certified-bound/independent_controls.py- Case file
frontier/n-017.md(verified lower, verified upper, reported lower, reported upper)