Discrete geometry · formal proof

Short of a Square

Remove c unit squares from a k × k grid. For small c the rest still needs a square of side k; for larger c, tilting lets them squeeze into a smaller one. Write c*(k) for the largest c with s(k² − c) = k. Every bound on this page is an explicit packing of k² − c squares in a square of side less than k, for every k in a range, checked by the Lean kernel.

Status. All theorems below are proved in Lean 4 with Mathlib, from the plain definition of a packing, using only the standard axioms (propext, Classical.choice, Quot.sound). Two of them are, as far as we know, new bounds; the others formalize results of Kevin Fang and Sungjoon Ryu, one of them on a wider range than its source. Not peer reviewed; the novelty check covers the jlevy/squares register and Ryu's preprint only.

kernel-checked in Lean, no hypothesis standard axioms only not peer reviewed Lean bundle on GitHub → every packing, drawn →

The theorems

Upper bounds on c*(k)

Each line is a Lean theorem ∀ k ≥ k₀, ∃ s < k, Packs (k·k − c) s, which gives c*(k) ≤ c − 1. Highlighted rows are new mathematics of ours; every Lean proof on this page is ours. The packings page shows where each one passes k² − k.

bound	for	Lean theorem · mathematics
c*(n) ≤ n − 2	n ≥ 15	FangFinal.theorem1 Kevin Fang, after Arslanov–Mustafin–Shangitbayev
+ p + 2q more squares	16p + 21q ≤ n − 15	FangFinal.theorem2 Fang
c*(k) ≤ 8⌈√(k − 4)⌉ − 1	k ≥ 6	RyuBound.packs_sub_8sqrt Ryu, Theorem 1.4
c*(k) ≤ 4⌈√(2k − 7)⌉ − 1	k ≥ 7	RyuLayers.packs_sub_4sqrt2_layers ours: axis-filled band ends (new)
c*(k) < 18.9 k^2/5 + 35.7 k^1/5 + 122	k ≥ 3·10⁵	RyuStairBound.packs_stair_k25 ours: Ryu's staircase ends, our count (new)
c*(k) < 20.668 k^2/5 + 0.623	k ≥ 8·10⁶	RyuStairBound.packs_ryu_thm12 Ryu, Theorem 1.2 (proved there for k ≥ 1.6·10⁷; the wider range is ours)

Which is smallest where: Fang's for 15 ≤ k ≤ 39; 4⌈√(2k − 7)⌉ − 1 from 40 to about 7.4·10⁵ (it is below Ryu's 8⌈√(k − 4)⌉ − 1 at every k ≥ 7); then the two-term k^2/5 bound, which is below Ryu's Theorem 1.2 bound for every k ≥ 6.7·10⁶. At small k the record packings of the register are better than any of these formulas, and Ryu's tuned certificates are better at the three k where he computed them; his k^3/8 bounds (not formalized here) take over for very large k.

k	Fang	8√ (Ryu)	4⌈√(2k−7)⌉ − 1	two-term k^2/5	Ryu Thm 1.2
100	90	79	55
10⁴	9 048	799	567
10⁵	90 476	2 535	1 791
10⁶	904 762	7 999	5 659	5 435
10⁷		25 303	17 891	12 943	13 041
10⁸		79 999	56 571	31 497	32 757

Entries are the resulting bounds on c*(k). Lower bounds are far smaller: c*(k) ≥ 3 for k ≥ 6, and Ryu's preprint claims c*(k) → ∞ (at least logarithmically).

The construction

An L of tilted rows

All the square-root and k^2/5 bounds use Ryu's L-shaped packing (after Erdős and Graham): an axis-parallel grid of (k − b)² squares, and two bands of rows of b squares each, tilted just enough that a row is a little narrower than b. The whole fits in side k − b + w < k. Each row is tilted, so successive rows are spaced slightly more than 1 apart, which costs about 2L/b along a band of length L: about 4k/b in all. The rest of the loss is at the four band ends, the triangles under the first row and over the last.

Schematic (not to scale): the grid, the two bands of tilted rows, and the four end regions (gold). The ends decide the constant. The actual packings, for every k up to 300: Packings row by row.

Empty ends

Each end wastes about b. Total ≈ 4b + 4k/b, best at b ≈ √k: Ryu's 8√k.

Axis-filled ends (new)

About b/2 axis-parallel squares fit under the first row and over the last. Total ≈ 2b + 4k/b, best at b ≈ √(2k): 4√2·√k ≈ 5.66√k. With b = ⌈√(2k − 7)⌉ the four ends hold exactly 2b squares.

Staircase ends

Columns at one tilt, axis layers under them that follow the rising ceiling, and short rows at the wall (Ryu's §6, after Bui). End cost O(b^2/3); with b ≈ k^3/5 the exponent is 2/5.

For the axis-filled ends, a search over every b and every axis layering of this construction finds nothing better than 4⌈√(2k − 7)⌉ − 1 for 7 ≤ k ≤ 3·10⁵. Better packings at small k exist but come from search (de Winter's, for example), not from a formula.

The proof

What Lean checks

The band and its ends. A band lifted by y₀, together with any packings of the two end regions, packs the strip (Ryu's Lemma 5.1, RyuEnds.band_ends); the three parts are separated by the rotated coordinate.
The staircase. Columns, layers and wedge rows pack an end region when each piece fits under the ceiling and the pieces are pairwise separated by one line (RyuStair.staircase). Our variant takes the column tilt tan(α/2) = (√2 + 1/v)/v with b ≈ v³, lets each layer run to the wall when it fits, and counts squares from the floors directly, with no area argument (EndP.count). The end cost is at most 4.33 v² + 11 v + 30 (end_bound); the leading 2√2 + 3/2 is Ryu's limit constant.
The count. k² − N is the slack of the side, plus (R − 1) tan θ per band, plus the four end costs (Ryu's waste identity, here an algebraic identity), which gives c*(k) < 4k/b + 4(4.33 v² + 11 v + 30) (packs_stair), and then the closed forms in k^2/5.
Fang's theorem is an induction over a gluing lemma (Arslanov–Mustafin–Shangitbayev's decomposition) with 18 exact piece certificates, each checked by decide in the kernel.

certificates/k2-minus-c/verify.sh          # Ryu-line theorems, a few minutes
certificates/k2-minus-c/verify.sh --fang   # also Fang's 18 pieces, ~20 min, ≤ 8 GB per job

Files: lean/Sqpack/RyuBand, RyuBound, RyuFill, RyuEnds, RyuLayers, RyuStair, RyuStairCount, RyuStairEnd, RyuStairBound, FangGlue, FangTheorem, FangFinal. Numerical companions in search/ryu/.

Credits

Whose mathematics

Original work

Sungjoon Ryu (squarepacker), k² − c upper bounds, preprint v1.1 (jlevy/squares #471, #486): the L-shaped family, the explicit square-root bound, the lifted rows and the waste identity, the staircase end and the k^2/5 and k^3/8 theorems.
H. D. Bui: tilted columns whose lower squares are replaced by axis layers, behind the staircase. Erdős and Graham (1975): the band construction.
Kevin Fang, Packing n² − n + 1 unit squares in a square of side less than n, for every n ≥ 15 (draft, jlevy/squares #603, registered as T-163), after Arslanov, Mustafin and Shangitbayev (2021), whose decomposition is his gluing lemma. His pieces are packings from the record lists, whose lineages run from Arslanov–Mustafin–Shangitbayev (2019) through Ellsworth, Cantrell, Stead, de Winter and others, and his own.

Ours (Evan Daniel, with Claude, October 2026)

New bounds: c*(k) ≤ 4⌈√(2k − 7)⌉ − 1 for every k ≥ 7 (the axis-filled band ends, their count and the choice of b), and c*(k) < 18.9 k^2/5 + 35.7 k^1/5 + 122 for every k ≥ 3·10⁵ (Ryu's staircase ends with our own count of the squares, no area argument). Filling the band ends with axis squares was suggested by a literature-reading agent of this project.
Formalization: every theorem on this page in Lean, from the plain definition of a packing. For Fang's theorems: the gluing lemma, the induction and exact certificates of all 18 pieces (with a rectangle checker); for Ryu's: simpler row counts, and his Theorem 1.2 from k ≥ 8·10⁶ instead of 1.6·10⁷.
The drawings on the packings page, re-checked against the theorems' counts.