T-236: Daniel reports Lean proofs of Fang's Theorems 1 and 2, s(n2−n+1)<n$s(n^2-n+1)<n$ for $n\ge 15$$n\ge 15$

The cases

Results on these cases

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

1. 2005 published T-007 · $n=211,241,273,307$$n=211,241,273,307$

   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$

   S3 V0 C1 Lower bound incomplete on these cases, superseded by T-083 and T-180 (reported)

   Nagamochi · Nagamochi 2005 · source · register

2. 2026-09-04 published T-085 · $n=211,241,273,307$$n=211,241,273,307$

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

   S3 V3 C3 Correction confirmed

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

3. 2026-09-16 published T-057 · $n=211$$n=211$

   $s(211)\le 14.99796070496771500150<15$$s(211)\le 14.99796070496771500150<15$, the first packing of 211 squares below the grid on record

   S3 V3 C3 Upper bound confirmed superseded by T-188

   de Winter · de Winter n211 2026-09-16 · packet · register

4. 2026-09-27 published T-056 · $n=241,273,307$$n=241,273,307$

   Smaller packings for 49 counts from $n=68$$n=68$ to $307$$307$, each certified two independent ways

   S3 V3 C3 Upper bound confirmed superseded by T-174, T-182 and T-256

   Couzo · franciscouzo square-packing 2026-09-27 · packet · register

5. 2026-09-29 published T-083 · $n=211,241,273,307$$n=211,241,273,307$

   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$

   S3 V3 C3 Lower bound confirmed

   Karakuş · Karakuş 2026 · source · register

6. 2026-10-05 published T-098 · $n=211,241,273,307$$n=211,241,273,307$

   Exact optima of 48 known-best packings: s(n) ≤ S', 3.5e-13 to 5.0e-11 below each printed side

   S2 V3 C3 Upper bound confirmed on these cases, superseded by T-174, T-182, T-188 and T-256

   Daniel after Couzo, de Winter, Ellsworth, Levy · evand exact optima 2026-10-05 · packet · register

7. 2026-10-09 published T-136 · $n=307$$n=307$

   Seventeen exact rational packings from SQUISH's third request

   S3 V3 C3 Upper bound confirmed superseded by T-256

   Chaoweeraprasit after Couzo, Xu, Göbel, Schadt, Ellsworth, Hajba, Levy · SQUISH third request 2026-10-09 · packet · register

8. 2026-10-11 published T-149 · $n=211$$n=211$

   New packings of 155, 156 and 211 squares, each with an exact rational certificate

   S3 V3 C3 Upper bound confirmed superseded by T-188

   Ostashev after Nakajima, Levy, Xu · Ostashev records 2026-10-11 · packet · register

9. 2026-10-12 published T-163 · $n=211,241,273,307$$n=211,241,273,307$

   s(n² − n + 1) < n for every n ≥ 15, and n² − n + F(n) squares below side n, from Fang

   S4 V3 C1 Upper bound reviewed superseded by T-174, T-182, T-188 and T-256

   Fang after Arslanov, Mustafin, Shangitbayev, Ellsworth, Stead, de Winter, Daniel, Couzo · Fang excess theorem 2026-10-13 · packet · packet · packet · source 1 · source 2 · register

10. 2026-10-13 published T-174 · $n=211,241,273,307$$n=211,241,273,307$

    Tighter certificates at 68 counts from PingYou Ltd, of others' packings and its own

    S1 V3 C3 Upper bound confirmed

    PingYou Ltd after Friedman, Ellsworth, Daniel, Xu, Barnett, Couzo, Ostashev, Chaoweeraprasit, Gupta, Fang, Polkovskyi, Levy · PingYou PR 574 certificates 2026-10-13 · packet · register

11. 2026-10-13 published T-175 · $n=211,241$$n=211,241$

    New packings of 211, 241 and 304 squares, two with merged tilted bands, each certified exactly

    S3 V3 C3 Upper bound confirmed superseded by T-182 and T-188

    Ostashev after Nakajima, Daniel, de Winter, Couzo, Levy, Xu · Ostashev merged bands 2026-10-13 · packet · register

12. 2026-10-13 published T-180 · $n=211,241,273,307$$n=211,241,273,307$

    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

    S4 V0 C1 Lower bound reviewed

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

13. 2026-10-13 published T-181 · $n=211,241$$n=211,241$

    Exact rational certificates at 211, 241 and 302 from Couzo

    S3 V3 C3 Upper bound confirmed superseded by T-182 and T-188

    Couzo after Daniel, Ostashev, Fang, Ellsworth, Levy; Couzo after Daniel, Ostashev, BuddenPing, Fang, Ellsworth, Levy · Couzo issue-583 certificates 2026-10-13 · Couzo certificates 2026-10-13 · packet · packet · register

14. 2026-10-13 published T-182 · $n=211,241$$n=211,241$

    Exact rational certificates at 154, 211 and 241 from Couzo

    S3 V3 C3 Upper bound confirmed

    Couzo after Daniel, Ostashev, BuddenPing, Fang, Ellsworth, Levy · Couzo certificates 2026-10-13 · packet · register

15. 2026-10-14 published T-188 · $n=211$$n=211$

    A tighter exact certificate for 211 squares from Couzo, of Ostashev's arrangement

    S2 V3 C3 Upper bound confirmed

    Couzo after Ostashev, Daniel, Levy · Couzo verified bounds 2026-10-14 · packet · register

16. 2026-10-18 published T-236 this result · $n=211,241,273,307$$n=211,241,273,307$

    Daniel reports Lean proofs of Fang's Theorems 1 and 2, s(n2−n+1)<n$s(n^2-n+1)<n$ for $n\ge 15$$n\ge 15$

    S3 V0 C0 Formalization recorded

    Daniel after Fang, Arslanov, Mustafin, Shangitbayev, Levy · Daniel Fang and Ryu Lean 2026-10-18 · packet · source · register

17. 2026-10-23 published T-253 · $n=211,241$$n=211,241$

    Polkovskyi's sub-print re-certifications of nine house packings, 1.3e-19 to 1.7e-19 below each

    S1 V0 C1 Upper bound reviewed

    Polkovskyi after Daniel, Couzo, Ostashev, de Winter, Chaoweeraprasit, Levy · Mishapolk refinements 2026-10-23 · packet · packet · register

18. 2026-10-28 published T-255 · $n=307$$n=307$

    Couzo's certificates of ntumlnoob's Kaggle packings at 260 and 307, below T-225 and T-174

    S3 V3 C3 Upper bound confirmed superseded by T-256

    Couzo after ntumlnoob, Daniel, Levy · Couzo a5a5d76 2026-10-28 · packet · packet · register

19. 2026-10-28 published T-256 · $n=307$$n=307$

    Couzo's packings from Kaggle notebook packings at 232, 260 and 307, below T-186, T-225 and T-174

    S3 V3 C3 Upper bound confirmed

    Couzo after Chilton, ntumlnoob, Lavrentev, Ellsworth, Daniel, Levy · Couzo issue 844 2026-10-28 · packet · register