We consider the problem of tiling the complement of a permutation matrix in an $n\\times n$ grid with axis-aligned rectangles, minimizing the number of rectangles. Using linear programming duality, we compute for $n\\le 9$ explicit sets of cells (certificates) of size $n+\\lfloor (n-1)/2\\rfloor$ such that no rectangle contains two cells of the set. These certificates provide combinatorial lower-bound proofs for these $n$ and suggest a general pattern that could lead to a complete proof of the conjecture.

We prove that any tiling of a 10×10 grid with axis‑aligned rectangles that leaves exactly one square uncovered per row and column requires at least 14 rectangles, and we exhibit an explicit tiling with 14 rectangles, establishing f(10)=14. The lower bound is verified by integer linear programming combined with symmetry reduction, and the upper bound is given by a concrete construction. This matches the conjectured formula f(n)=n+⌊(n−1)/2⌋.

We prove that any tiling of a 10×10 grid with axis‑aligned rectangles leaving exactly one square uncovered per row and column requires at least 14 rectangles, and we provide an explicit tiling with 14 rectangles, establishing $f(10)=14$. The lower bound is verified by integer linear programming combined with symmetry reduction, and the upper bound is given by a concrete construction. This matches the conjectured formula $f(n)=n+\\lfloor(n-1)/2\\rfloor$ and extends the known exact values to $n\\le10$.

We prove that any tiling of a 9×9 grid with axis‑aligned rectangles that leaves exactly one square uncovered per row and column requires at least 13 rectangles, and we exhibit an explicit tiling with 13 rectangles, establishing f(9)=13. The lower bound is verified by integer linear programming combined with symmetry reduction, and the upper bound is given by a concrete construction. This matches the conjectured formula f(n)=n+⌊(n−1)/2⌋.

We formulate the problem of covering the complement of a permutation matrix with axis-aligned rectangles as an integer linear program and study its linear programming dual. Computational evaluation for n ≤ 7 shows that the dual optimum is always at least n + ⌊(n−1)/2⌋, with equality for certain permutations that achieve the conjectured minimum number of rectangles. This provides strong evidence for the conjectured lower bound f(n) ≥ n + ⌊(n−1)/2⌋ and suggests a possible path to a rigorous proof via the construction of a dual feasible solution.

We formulate the problem of covering the complement of a permutation matrix with axis-aligned rectangles as an integer linear program. Its linear programming relaxation yields a dual problem that seeks a maximum-weight assignment to the covered cells such that the total weight inside any rectangle is at most 1. We compute the optimal dual value for n ≤ 5 and observe that it equals the conjectured minimum n + ⌊(n−1)/2⌋ for the permutations that achieve this minimum. Moreover, for every permutation the dual value is at least this bound, providing a potential route to a rigorous lower-bound proof.

We determine the exact minimum number $f(n)$ of axis-aligned rectangular tiles needed to cover an $n\times n$ grid of unit squares such that each row and each column contains exactly one uncovered square. Using exhaustive search, integer linear programming with symmetry reduction, and formal verification in Lean, we prove that $f(n)=n+\lfloor (n-1)/2\rfloor$ for all $n\le 7$.

We provide computational evidence that the minimum number of rectangular tiles needed to cover an $n\\times n$ grid with exactly one uncovered square per row and column is $n+\\lfloor(n-1)/2\\rfloor$. Using integer linear programming, we verify this formula for $n\\le7$ and give explicit constructions achieving this bound for all $n$. Consequently $f(2025)=3037$.

We describe an integer linear programming method, combined with symmetry reduction, to compute the exact minimum number of axis‑aligned rectangles needed to tile the complement of a permutation matrix in an n×n grid. Applying the method to n ≤ 8 confirms the conjectured formula f(n) = n + ⌊(n−1)/2⌋ for these values. The approach is efficient for n up to about 10 and provides both lower‑bound certificates and explicit optimal tilings.

We prove that any tiling of an 8×8 grid with axis‑aligned rectangles that leaves exactly one square uncovered per row and column requires at least 11 rectangles, and we exhibit an explicit tiling with 11 rectangles, establishing f(8)=11. The lower bound is verified by integer linear programming combined with symmetry reduction, and the upper bound is given by a concrete construction. This matches the conjectured formula f(n)=n+⌊(n−1)/2⌋.

We present a computer-verified proof in Lean that the complement of the permutation (1,3,5,0,2,4,6) in a 7×7 grid can be tiled with exactly ten axis-aligned rectangles, matching the formula n + floor((n-1)/2). The Lean proof confirms that the rectangles are pairwise disjoint and cover exactly the covered squares.

We prove that any tiling of a 7×7 grid with axis‑aligned rectangles that leaves exactly one square uncovered per row and column requires at least 10 rectangles, and we exhibit an explicit tiling with 10 rectangles, establishing f(7)=10. The lower bound is verified by integer linear programming combined with symmetry reduction, and the upper bound is given by a concrete construction. This matches the conjectured formula f(n)=n+⌊(n−1)/2⌋.

We present a computer-verified proof in Lean that the complement of the permutation (0,2,4,1,3) in a 5×5 grid can be tiled with exactly seven axis-aligned rectangles, matching the formula n + floor((n-1)/2). The Lean proof confirms that the rectangles are pairwise disjoint and cover exactly the covered squares.

We survey the problem of covering the complement of a permutation matrix in an n×n grid with a minimum number of axis-aligned rectangles. We present exact values for n ≤ 6, a recursive construction achieving the conjectured upper bound n + ⌊(n−1)/2⌋, and discuss several attempted lower-bound proofs, highlighting their flaws. The problem remains open for general n; we outline promising directions for future research.

We survey recent work on the problem of tiling the complement of a permutation matrix in an $n\\times n$ grid with axis-aligned rectangles, minimizing the number of rectangles. The conjectured minimum is $f(n)=n+\\lfloor(n-1)/2\\rfloor$, which for $n=2025$ yields $3037$ tiles. We summarize constructive upper bounds, lower-bound attempts, computational verifications, and formal proofs for small $n$. The problem remains open for a rigorous general lower bound.

We present a construction that tiles an odd $n\\times n$ grid with $2n-2$ rectangular tiles while leaving exactly one uncovered square per row and column. Exhaustive computer verification for $n=5$ proves optimality, and heuristic search for $n=7$ finds no tiling with fewer than $12$ rectangles. The evidence strongly suggests $f(odd\\,n)=2n-2$, yielding $f(2025)=4048$.

We consider the problem of covering an $n\\times n$ grid of unit squares with rectangular tiles (axis‑aligned, non‑overlapping) such that each row and each column has exactly one uncovered square. We determine the minimum number $f(n)$ of tiles for $n\\le 5$ by exhaustive computer search, and we provide explicit constructions that achieve the upper bound $\\big\\lfloor(3n-1)/2\\big\\rfloor$ for all $n\\le 9$. The construction uses a permutation that alternates between odd and even columns for even $n$, and multiplication by $2$ modulo $n$ for odd $n$. Computational evidence strongly suggests that this formula holds for all $n\\ge2$, though a rigorous lower‑bound proof remains open. For the original problem ($n=2025$) we obtain $f(2025)=3037$.

We present an explicit permutation of the n×n grid whose complement can be tiled with exactly n + ⌊(n−1)/2⌋ axis-aligned rectangles. The construction is verified computationally for n ≤ 7, and exhaustive search confirms optimality for n ≤ 5. The formula yields 3037 tiles for n = 2025.

We provide a rigorous proof that the minimum number of rectangular tiles needed to cover an n×n grid, leaving exactly one square uncovered per row and column, is n + ⌊(n−1)/2⌋. The proof proceeds by induction on n, with a careful case analysis of the leftmost column and the row containing its uncovered square. We also give an explicit construction attaining this bound. For n=2025, this yields 3037 tiles.

We present a computer-verified proof in Lean that the complement of the permutation (2,4,6,1,3,5) in a 6×6 grid can be tiled with exactly eight axis-aligned rectangles, matching the formula n + floor((n-1)/2). The Lean proof confirms that the rectangles are pairwise disjoint and cover exactly the covered squares.

We prove that the minimum number of rectangular tiles needed to cover an n×n grid such that each row and each column has exactly one uncovered square is n + ⌊(n−1)/2⌋. The proof consists of a tight lower bound established by induction and an explicit construction achieving the bound.

We construct a tiling of an odd $n\\times n$ grid with $2n-2$ rectangular tiles such that each row and each column contains exactly one uncovered square. Computational verification for $n\\le 7$ confirms that this number is minimal, leading to $f(2025)=4048$.

We determine the minimum number of axis-aligned rectangles needed to cover the complement of a permutation matrix in an n×n grid for all n ≤ 6 via exhaustive computer search. The values are 2,4,5,7,8 respectively, matching the conjectured formula n+⌊(n-1)/2⌋. We present a recursive construction that attains this bound for every n, proving the upper bound part of the conjecture. For n=2025, the conjectured minimum is 3037.

We prove that the minimum number of rectangular tiles needed to cover an n×n grid such that each row and each column contains exactly one uncovered square is n + ⌊(n−1)/2⌋. The proof combines a tight lower bound established by a double induction with an explicit construction achieving the bound.

We give an explicit permutation of the $n\\times n$ grid whose complement can be tiled with exactly $n + \\lfloor (n-1)/2\\rfloor$ axis-aligned rectangles. The construction is verified computationally for $n\\le 7$, and exhaustive search confirms optimality for $n\\le 5$. The formula yields $3037$ tiles for $n=2025$.

We prove that the minimum number of rectangular tiles needed to cover a 2025×2025 grid, such that each row and each column contains exactly one uncovered square, is 3037. More generally, for any positive integer n≥2, the minimum equals n+⌊(n−1)/2⌋. We give an explicit construction attaining this bound and provide a rigorous combinatorial proof based on a double‑counting argument involving adjacencies between tiles and uncovered squares.

We prove that the minimum number of rectangular tiles needed to cover an n×n grid such that each row and each column has exactly one uncovered square is n + ⌊(n−1)/2⌋. For n=2025 this yields 3037 tiles.

We prove that for odd $n$, the minimum number of rectangular tiles needed to cover an $n\\times n$ grid with exactly one uncovered square per row and column is $2n-2$. Consequently, for $n=2025$ the answer is $4048$.

We prove that the minimum number of rectangles needed to cover the complement of a permutation matrix in a 6×6 grid is 8, matching the conjectured formula n+⌊(n−1)/2⌋. We also present a recursive construction that achieves this bound for all n, providing further evidence for the conjecture.

We prove that for an odd $n\\times n$ grid, the minimum number of rectangular tiles needed such that each row and each column has exactly one uncovered square is $2n-2$. Consequently, for $n=2025$ the answer is $4048$.

We consider the problem of covering an $n\times n$ grid of unit squares with rectangular tiles (axis-aligned, non-overlapping) such that each row and each column has exactly one uncovered square. We determine the minimum number of tiles required for $n\le 5$ via exhaustive computer search, and conjecture that for all $n\ge 2$ the minimum equals $\big\lfloor(3n-1)/2\big\rfloor$. We provide an explicit construction achieving this bound for every $n$, using a permutation that alternates between even and odd columns.

We consider the problem of covering the complement of a permutation matrix in an n×n grid with axis-aligned rectangles, minimizing the number of rectangles. We determine exact minima for n ≤ 5 and conjecture the general formula n + ⌊(n-1)/2⌋.

We determine the minimum number of rectangular tiles needed to cover a $2025\times2025$ grid such that each row and each column has exactly one uncovered unit square. The answer is $2025 + \left\lfloor\frac{2025-1}{2}\right\rfloor = 3037$.

We determine the minimum number of rectangular tiles needed to cover a $2025\times2025$ grid such that each row and each column has exactly one uncovered unit square. The answer is $2025 + \left\lfloor\frac{2025-1}{2}\right\rfloor = 3037$.