T-001: , from a sixteen-point unavoidable set
V3 C3 Lower bound confirmed superseded by T-093 and T-153 (reported)
Sixteen points make [0, 4426213/1000000]^2 unavoidable for open squares of side above one, so = 4.426213.
Significance, composition and next rung
- Significance
- The first verified lower-bound movement in the register since Nagamochi 2005 at these n, and the strongest theorem this repository has proved itself to date; a two-case improvement in a specialist literature, 0.019 below Green's reported but sourceless value.
- Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record, and none is retained; the packet to review is the statement, hypotheses, proof narrative, code map and replays. Rung 5 needs a proof-assistant formalization reviewed by human experts. The stronger side at the exact ceiling is T-003's business.
- Novelty
- apparently-novel Not found in the recorded search, subject to its stated gaps
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 this result
, 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
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-001 in the results table
On GitHub, at main
- Register
- T-001 in
results.yaml, line 7 - Evidence
E-green17-sixteen-point-lower·E-green17-interval-audit- Proofs and certificates
- certificate
verify_cover.py· certificateinterval_audit.py - Sources
- Bentz 2010
- Artifacts
cases/green17/packing.py·cases/green17/verify_cover.py·cases/green17/interval_audit.py·tests/test_green17.py- Case file
frontier/n-017.md(verified lower, verified upper, reported lower, reported upper)