---

Claim. Let $L_{k,n}$ be the number of $k\times n$ Latin rectangles with labeled rows, columns and symbols. The manuscript states that for every $k=o(n)$,

$$L_{k,n}\sim(n!)^k\Bigl(\frac{(n)_k}{n^k}\Bigr)^n \Bigl(1-\frac kn\Bigr)^{-n/2}e^{-k/2},$$

the formula Godsil and McKay established for $k=o(n^{6/7})$, where $(n)_k=n(n-1)\cdots(n-k+1)$. Its sharper form replaces the last two factors by $\exp\{[n(H_n-H_{n-k})-k]/2\}$, with $H_m$ the $m$th harmonic number, and asserts that for every function $K(n)=o(n)$ the ratio of $L_{k,n}$ to this normalization has logarithm $O(k^2/n^2)$, uniformly for $0\le k\le K(n)$ and with an absolute implied constant. As the forum entry describes the argument, an asymptotic for the permanent of a matrix whose entries are all near $1$ (through a Gamma-function representation and a cluster expansion in which the cycles are isolated) is combined with a path-switching argument that controls the second-moment statistics left over, and the ratios obtained for adding one row to a rectangle are multiplied together.

Submission note. Posted to erdosproblems.com as a proof claim by Eric Li (account EricLi) on 4 August 2026, giving "GPT-5.6 Sol Pro, Codex" as the AI used:

The paper partially solves Erdős Problem 725 by proving that the number $ L_{k,n} $ of ordered $ k\times n $ Latin rectangles obeys the Godsil–McKay asymptotic

$$> (n!)^k\Bigl(\frac{(n)_k}{n^k}\Bigr)^n\Bigl(1-\frac{k}{n}\Bigr)^{-n/2}e^{-k/2} >$$

for every $ k=o(n) $, extending the earlier range $ k=o(n^{6/7}) $. A refined normalisation $ \widetilde A_{k,n} $ satisfies $ \log(L_{k,n}/\widetilde A_{k,n})=O(k^2/n^2) $ uniformly on any sublinear range. The proof combines a permanent asymptotic for matrices close to the all-ones matrix (via a Gamma representation and cluster expansion isolating cycles) with a path-switching argument that controls residual second-moment statistics, then multiplies the resulting one-row extension ratios. Notes: This partial proof has been formally verified in Lean.

Covers. The asymptotic count on every range $k\le K(n)$ with $K(n)=o(n)$, extending the ranges of Erdős and Kaplansky [ErKa46], Yamamoto [Ya51] and Godsil and McKay [GoMc90]. It leaves open the count when $k$ is a positive proportion of $n$, including the number of Latin squares ($k=n$), so Problem 725, which asks for an asymptotic formula without restricting $k$, is not settled by it.

Claimant. Eric Li, who posted the manuscript on arXiv on 3 August 2026 (v1, 25 pages) and the claim on the site's forum on 4 August 2026. The forum entry names GPT-5.6 Sol Pro and Codex as its tools.

Formalization. The author's repository declares itself a Lean formalization of the manuscript's results, so it is linked here, pinned to a commit. Its README reports that the main theorem is proved for every prescribed sublinear bound, that no source file uses sorry, admit, native_decide or a project axiom, and that its exported endpoints were audited for axioms. This corpus has not built or audited the development.

Acceptance. None that counts as evidence. The manuscript is not refereed (the arXiv record lists no journal reference), the forum entry carried no comments no outside reviewer has endorsed the proof, and the site labels the problem OPEN with commentary that does not name the manuscript. This corpus has not built the Lean development, so no formalized evidence is listed. The manuscript is not held; this account follows the arXiv abstract, the forum entry and the repository README.