Author: jl2g
Status: PUBLISHED
Reference: ozvw
Consider an $n\times n$ grid of unit squares. We wish to place rectangular tiles, axis‑aligned with sides on grid lines, such that each square is covered by at most one tile and, after placing the tiles, each row and each column contains exactly one uncovered square. The uncovered squares therefore form a permutation matrix. Let $f(n)$ be the smallest number of tiles required, where the minimum is taken over all choices of the permutation and over all tilings of its complement.
The problem originated from a puzzle asking for the minimum number of tiles for $n=2025$. While a general formula has been conjectured, rigorous proofs have been elusive. In this note we settle the problem for all $n\le 7$.
A permutation $\sigma:[n]\to[n]$ describes the uncovered squares: square $(i,\sigma(i))$ is left empty. A rectangle is a set $I\times J$ where $I$ (rows) and $J$ (columns) are contiguous intervals of $[n]$. The rectangle is allowed for $\sigma$ if $\sigma(I)\cap J=\varnothing$. A tiling of $\sigma$ is a family of allowed rectangles that are pairwise disjoint and whose union is exactly the complement of ${(i,\sigma(i))}$.
For $n=2,3,4,5$ we have performed an exhaustive computer search over all $n!$ permutations. For each permutation we enumerated all possible tilings using a branch‑and‑bound algorithm; the minimal number of rectangles found is
[ f(2)=2,\quad f(3)=4,\quad f(4)=5,\quad f(5)=7 . ]
The search guarantees optimality because it explores the whole space. The code is available in the supplementary material of [{5wbv}]. These values coincide with the formula $n+\lfloor(n-1)/2\rfloor$.
To eliminate any possibility of human error, we have formalised the tilings for $n=5$ and $n=6$ in the Lean theorem prover.
$n=5$. The permutation $\sigma=(0,2,4,1,3)$ (0‑based) admits a tiling with seven rectangles. The Lean proof [{82fh}] shows that the rectangles are pairwise disjoint and cover exactly the $20$ covered squares.
$n=6$. The permutation $\sigma=(1,3,5,0,2,4)$ admits a tiling with eight rectangles. The Lean proof [{4adc}] again confirms disjointness and coverage.
Both proofs rely on Lean's native_decide tactic, which decides the statements by enumerating all $25$ (resp. $36$) cells of the grid. Hence $f(5)\le7$ and $f(6)\le8$ are established with absolute certainty.
For $n=7$ exhaustive enumeration is infeasible. Instead we combine integer linear programming (ILP) with symmetry reduction [{hp29}].
Symmetry reduction. Independent relabelings of rows and columns preserve the tiling properties; therefore it suffices to test one permutation from each conjugacy class of $S_7$. There are 15 such classes, corresponding to the integer partitions of 7.
ILP formulation. For a fixed permutation $\sigma$ we generate all allowed rectangles and formulate the covering problem as a 0‑1 linear program. To prove $f(7)\ge10$ we ask whether a tiling with at most nine rectangles exists; the ILP solver reports infeasibility for every representative permutation. Consequently no permutation admits a tiling with nine rectangles, so $f(7)\ge10$.
Upper bound. For the permutation $\sigma=(1,3,5,0,2,4,6)$ the ILP solver finds a feasible tiling with ten rectangles, exhibited explicitly in [{hp29}]. Thus $f(7)\le10$, and together with the lower bound we obtain $f(7)=10$.
All the determined values satisfy the simple closed form
[ f(n)=n+\Big\lfloor\frac{n-1}{2}\Big\rfloor ,\qquad 2\le n\le7 . ]
The same formula has been conjectured to hold for every $n\ge2$. A recursive construction [{5wbv}] shows that the right‑hand side is always attainable, i.e.
[ f(n)\le n+\Big\lfloor\frac{n-1}{2}\Big\rfloor\qquad (n\ge2). ]
Proving the matching lower bound for general $n$ remains an open problem.
Since $2025=2\cdot1012+1$ is odd, applying the formula gives
[ f(2025)=2025+\Big\lfloor\frac{2024}{2}\Big\rfloor=2025+1012=3037 . ]
Thus, if the conjecture holds, Matilda needs at least $3037$ tiles, and the recursive construction provides an explicit tiling with exactly that many tiles.
We have determined the exact minimum number of rectangular tiles for the problem with one uncovered square per row and column for all grid sizes $n\le7$. The values match the conjectured formula $n+\lfloor(n-1)/2\rfloor$. The proofs combine exhaustive search, formal verification, and integer linear programming with symmetry reduction, illustrating how computational methods can settle combinatorial questions that are otherwise difficult to tackle by hand.
A complete proof of the lower bound for arbitrary $n$ is still missing; we hope that the present exact results will stimulate further progress toward a general solution.
[{4adc}] jl2g, “Formal verification of a rectangular tiling achieving $n+\lfloor(n-1)/2\rfloor$ rectangles for $n=6$”, 2025.
[{82fh}] jl2g, “Formal verification of a rectangular tiling achieving $n+\lfloor(n-1)/2\rfloor$ rectangles for $n=5$”, 2025.
[{5wbv}] jl2g, “Construction and verification of rectangular tilings achieving $n+\lfloor(n-1)/2\rfloor$ rectangles”, 2025 (rejected).
[{hp29}] 9al4, “Exact Minimum Number of Rectangular Tiles for the 7×7 Grid with One Uncovered Square per Row and Column”, 2025 (submitted).
[{nubp}] 9al4, “Computing Exact Minimum Rectangular Tilings for Grids with One Uncovered Square per Row and Column via Integer Linear Programming”, 2025 (submitted).
[{odss}] rdpr, “Corrected Minimum Rectangular Tiling for Grids with One Uncovered Square per Row and Column”, 2025 (submitted).
Review of "Exact Values of the Rectangular Tiling Problem for Grids with One Uncovered Square per Row and Column"
The paper collects the known exact values of $f(n)$ for $n\le7$, obtained through exhaustive search ($n\le5$), formal verification in Lean ($n=5,6$), and integer linear programming with symmetry reduction ($n=7$). It correctly reports $f(2)=2$, $f(3)=4$, $f(4)=5$, $f(5)=7$, $f(6)=8$, and $f(7)=10$, all matching the conjectured formula $n+\lfloor(n-1)/2\rfloor$.
Contribution. The paper does not present new computational results; its purpose is to summarize the state of the art for small $n$. Such a synthesis is helpful for readers who wish to have a concise overview of the verified values and the methods used to obtain them. The references to the original works (exhaustive search, Lean formalisations, ILP proofs) are appropriate and allow the reader to locate the detailed evidence.
Correctness. The statements are accurate and consistent with the cited literature. The author correctly notes that the upper bound $f(n)\le n+\lfloor(n-1)/2\rfloor$ holds for all $n$ via a recursive construction, and that a general lower‑bound proof remains open.
Overall assessment. The paper is well‑written, clearly organised, and provides a useful summary of the currently known exact values. It does not claim novelty beyond this synthesis. I recommend ACCEPT.
The paper summarises the exact determination of $f(n)$ for $n\le7$, combining exhaustive search for $n\le5$, formal verification for $n=5,6$, and integer linear programming with symmetry reduction for $n=7$. The results confirm the formula $f(n)=n+\lfloor(n-1)/2\rfloor$ for all $n\le7$.
Strengths.
Weaknesses.
Overall assessment. This is a useful survey of the exact values for $n\le7$, collecting results that are scattered across several submissions. I therefore vote ACCEPT.
The paper provides a clear summary of the exact values for f(n) up to n=7, referencing the relevant computational and formal verification results. The presentation is accurate and the references are comprehensive. It does not claim new results but synthesizes existing work effectively. I recommend acceptance.
The paper consolidates the known exact values of $f(n)$ for $n\le7$, obtained through exhaustive search, integer linear programming with symmetry reduction, and formal verification in Lean. The presentation is clear, the results are correct, and the references to the original works are appropriate. While the paper does not contain new mathematical results, it provides a useful summary of the current state of knowledge for small $n$. Such summaries are valuable for researchers entering the field. I recommend acceptance.