c*(k) · the packings, row by row

Packings Row by Row

Row k holds every count n from (k − 1)² + 1 to k², right-aligned, so the column counted from the right is the deficit c = k² − n. Each Lean-checked construction gives one packing per row: k² − c squares in a square of side less than k. Its cell shows that packing in miniature, and every cell to its left follows by deleting squares. Hover a cell to see it larger; click to open the packing, then step to the next one in its series.

side k is needed (proved) open packed below side k only by a search record follows from a construction (tint: the best one in that row) the best known packing (any method) n = k² − k: cells to its right beat it

Loading Fang's pieces…

a landmark

Beating k² − k

Is s(k² − k) < k? That is, can a k × k grid lose one full row and have the rest fit in a smaller square? It is the bold line in the triangle. Erdős and Graham's waste bound (1975) passes it for all sufficiently large k, with no explicit threshold; otherwise it was known only at single k until Arslanov, Mustafin and Shangitbayev reached it for every k ≥ 12. Fang was the first to pass it for every k from an explicit start (15). The chart counts the squares beyond k² − k that each construction packs in side < k: above zero beats the line. The filled L-shape (ours) beats it for every k ≥ 37 (first at 33), Ryu's square-root bound from k ≥ 73; both margins grow like k − O(√k), against Fang's ≈ 2k/21.

when	who	what, relative to k² − k
1975	P. Erdős, R. L. Graham	beats it for all sufficiently large k (wasted area O(k^7/11)), no explicit threshold
1991–98	Lars Cleemann	reaches it at k = 17: s(272) < 17
2015	Károly Hajba	reaches it at k = 16: s(240) < 16
2019 (EJC 2021)	M. Z. Arslanov, S. A. Mustafin, Z. K. Shangitbayev	reaches it for every k ≥ 12, and beats it by one square at k = 16, 17, 18 (refereed)
2025	David W. Cantrell	reaches it at k = 11: s(110) < 11, the smallest such k known
2026	Kevin Fang	beats it for every k ≥ 15, by 1 + p + 2q squares (draft, jlevy/squares #603)
2026	Sungjoon Ryu	the L-shape: beats it by k − 8⌈√(k − 4)⌉, for every k ≥ 73 (preprint)
2026-10	ours (Evan Daniel, with Claude)	all of the above constructions checked in Lean; the filled L-shape beats it by k − 4⌈√(2k − 7)⌉, for every k ≥ 37
2024–26	record searches: Ellsworth, Stead, de Winter, Couzo, Ostashev, Mishapolk, Fang, us and others	single-k packings, best known up to k = 40 (the rings): up to 8 squares beyond the line
open		4 ≤ k ≤ 10: whether s(k² − k) < k at all

Dates and finders before 2026 as Erich Friedman's and David Ellsworth's catalogue records them; later ones from the jlevy/squares register and issues.

Fang's gluing original

k² − k + 1 + p + 2q in side < k, k ≥ 15, 16p + 21q ≤ k − 15

Kevin Fang's theorem, after Arslanov, Mustafin and Shangitbayev: a base piece of side 15 to 30, then 17 × 16 and 22 × 21 rectangles (257 and 443 squares) glued on, each with aligned blocks. Linear: about k − 1 − 2(k − 15)/21. Best here for 15 ≤ k ≤ 39. Lean: FangFinal.theorem2.

maths: Kevin Fang (2026 draft); the gluing lemma is Arslanov–Mustafin–Shangitbayev's decomposition (2021). Pieces: packings from the record lists, whose lineages run from Arslanov–Mustafin–Shangitbayev (2019) through Ellsworth, Cantrell, Stead, de Winter and others, and Fang's own.
Lean: ours: the gluing lemma, the induction, and exact certificates of all 18 pieces (a rectangle checker for the two rectangles).

Ryu's L-shape original

c*(k) ≤ 8⌈√(k − 4)⌉ − 1, k ≥ 6

Sungjoon Ryu's Theorem 1.4: an axis grid of side k − b and two bands of rows of b squares, tilted just past 2 arctan(1/b), so each row is a little narrower than b. The band ends are left empty. Lean: RyuBound.packs_sub_8sqrt.

maths: Sungjoon Ryu (2026 preprint, jlevy/squares #471, #486); the bands go back to Erdős and Graham (1975).
Lean: ours, with simpler row counts (exactly 8b squares short).

The filled L-shape ours · new

c*(k) ≤ 4⌈√(2k − 7)⌉ − 1, k ≥ 7

Ryu's L-shape with b = ⌈√(2k − 7)⌉ and axis squares in the four band ends (green in the viewer): 2b of them in all. Best here from k = 40 to about 7.4 · 10⁵. As far as we know a new bound. Lean: RyuLayers.packs_sub_4sqrt2_layers.

maths: ours (Evan Daniel, with Claude, October 2026): the end fills, their count and the choice of b, on Ryu's L-shape. Filling the ends with axis squares was suggested by a literature-reading agent of this project.
Lean: ours.

Also ours, not drawn here: the staircase bound c*(k) < 18.9 k^2/5 + 35.7 k^1/5 + 122 (k ≥ 3 · 10⁵; Ryu's staircase ends with our count) and Ryu's Theorem 1.2 in Lean on a wider range (k ≥ 8 · 10⁶, against 1.6 · 10⁷ in his proof). See the write-up.

Reading the triangle

A construction's cell is the packing its theorem gives: in row k, column c, it packs k² − c squares in side < k, so c*(k) ≤ c − 1. The cells to its left are the same packing with squares deleted.
Green cells are where side k is proved necessary: the grid families s(k² − c) = k for c ≤ 4 (for c = 3 from k = 6, c = 4 from k = 5), and every n ≤ 324 whose lower bound has reached k (some of those proofs are from 2026 and unrefereed). Open cells are where neither a packing below side k nor such a proof is known.
The ring is the best known packing below side k by any method, from the jlevy/squares register and the packings reported on its issues (some not yet accepted there), up to k = 40. Those are search results and are not drawn here. Beyond k = 40 the constructions are all that is known.
Drawings are floating point. The exact statements are the Lean theorems; search/ryu/explorer_check.mjs re-checks every drawing on this page (count equal to the theorem's, side < k, no overlaps) for k ≤ 400.
Not drawn: the staircase bound c*(k) < 18.9 k^2/5 + 35.7 k^1/5 + 122, which starts at k = 3 · 10⁵ (see the write-up).