T-250: Hosono reports a Lean kernel proof of Daniel's Valid7, and so of s(k2−3)=k$s(k^2-3)=k$ for every $k\ge 6$$k\ge 6$

2005 published T-007 · 13 of these cases

s(n)≥min(⌈n​⌉,n−2⌊n​⌋+1​+1)$s(n)\ge min(\lceil \sqrt{n}\rceil ,\sqrt{n-2\lfloor \sqrt{n}\rfloor +1}+1)$ for $4\le n\le 324$$4\le n\le 324$

Lower bound incomplete on these cases, superseded by T-008, T-063, T-064 and T-067

Nagamochi · Nagamochi 2005 · source · register

2010-09-13 published T-004 · case 46

Bentz 2010, Theorem 8 ($s(46)\ge 7$$s(46)\ge 7$) is correct as printed, machine-audited in full

Audit confirmed

Bentz · Bentz 2010 · source · register

2010-09-13 published T-008 · case 46

$s(46)=7$$s(46)=7$

Optimality confirmed

Bentz · Bentz 2010 · source · register

2018 published T-087 · case 61

s(37)≥53​/2+22​−1$s(37)\ge 5\sqrt{3}/2+2\sqrt{2}-1$ and s(61)≥73​/2+22​−1$s(61)\ge 7\sqrt{3}/2+2\sqrt{2}-1$, by optimal piercing

Lower bound reviewed superseded by T-063

Bašić, Slivková · Basic-Slivkova 2018 · source · register

2026-09-04 published T-085 · 13 of these cases

Nagamochi 2005, Lemma 1 is false for every container with $a>3$$a>3$ and $b>2$$b>2$

Correction confirmed

Karakuş; Vlasenko · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register

2026-09-27 published T-045 · cases 61, 78

Rectangle-density lower bounds replayed at 15 counts in $n=18\dots 78$$n=18\dots 78$

Lower bound confirmed superseded by T-063, T-064 and T-067

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · packet · packet · source · review · register

2026-09-27 published T-046 · cases 61, 78

Rectangle-density lower bounds verified at 48 counts in $n=18\dots 95$$n=18\dots 95$

Lower bound confirmed superseded by T-063, T-064 and T-067

Hosono after Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 rectangle bounds 2026 · wand125 rectangle bounds 2026-09-28 · packet · packet · source · review · register

2026-09-28 published T-063 · case 61

$s(61)=8$$s(61)=8$, by monotonicity from T-062

Optimality confirmed

Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · register

2026-09-29 published T-058 · 5 of these cases

Rectangle-certificate ceiling α·UB(n) proved for $n=1$$n=1$..100; B·UB(n) on 64 grid rows

Method limit confirmed

Hosono after Tokoharu, Daniel · wand125 tools 2026 · packet · register

2026-09-29 published T-083 · 13 of these cases

s(n)≥1/2+n−⌊n​⌋+1/4​$s(n)\ge 1/2+\sqrt{n-\lfloor \sqrt{n}\rfloor +1/4}$ for every nonsquare $8\le n\le 324$$8\le n\le 324$

Lower bound confirmed on these cases, superseded by T-008, T-063, T-064 and T-067

Karakuş · Karakuş 2026 · source · register

2026-09-30 published T-064 · 13 of these cases

s(k2−3)=k$s(k^2-3)=k$ for every integer $k$$k$ from 6 up; $k=6\dots 18$$k=6\dots 18$ are the cases held here

Optimality confirmed

Daniel after Burns, Massaccesi · evand square-packing 2026-10-01 · packet · packet · packet · packet · source 1 · source 2 · review 1 · review 2 · register

2026-10-01 published T-067 · case 78

$s(77)=9$$s(77)=9$, by a mixed cover extended from Daniel's $s(60)$$s(60)$ cover

Optimality confirmed

Hosono after Daniel, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 exact covers 2026-10-01 · packet · source · review · register

2026-10-07 published T-124 · 13 of these cases

Reported non-strict local minima for 178 source configurations

Restricted optimality recorded

Daniel after Couzo · Daniel exact and local reports 2026 · packet · register

2026-10-12 published T-261 · 13 of these cases

Reported grade-C local minima for 233 source configurations of field degree at most 4

Restricted optimality incomplete

Daniel after Schadt, Ellsworth, Levy · Daniel exact and local reports 2026-10-12 · packet · packet · register

2026-10-13 published T-180 · 11 of these cases

Closed-form lower bound $s(N)\ge a(N)$$s(N)\ge a(N)$ for every non-square $N\ge 49$$N\ge 49$, reported

Lower bound reviewed on these cases, superseded by T-063, T-064 and T-067

Hosono · wand125 closed form 2026-10-14 · packet · packet · register

2026-10-17 published T-250 this result · 13 of these cases

Hosono reports a Lean kernel proof of Daniel's Valid7, and so of s(k2−3)=k$s(k^2-3)=k$ for every $k\ge 6$$k\ge 6$

Formalization recorded

Hosono after Daniel, Burns, Massaccesi; Hosono after Daniel, Levy, Burns, Massaccesi · wand125 Valid7 Lean 2026-10-11 · wand125 Valid7 Lean v2 2026-10-17 · packet · packet · source 1 · source 2 · register