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 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.