---

Claim. Let $t(n)$ be the least number of points of $\{1,\ldots,n\}^2$ whose pairwise connecting lines cover every point of $\{1,\ldots,n\}^2$. Then

$$t(n) \ll n^{2/3} \log n ,$$

so $t(n) = o(n)$, which answers the question of Problem 798 in the affirmative. Together with the lower bound $t(n) \gg n^{2/3}$ of Erdős and Purdy, this determines the order of $t(n)$ up to a factor of $\log n$; the paper proves the same two bounds in every dimension $d \ge 2$, with exponent $d(d-1)/(2d-1)$ in place of $2/3$ (Theorem 1.1). The upper bound combines a geometric and probabilistic argument with tools from Diophantine approximation.

Source. N. Alon, Economical coverings of sets of lattice points, Geom. Funct. Anal. 1 (1991), no. 3, 225–230, September 1991 (the page range as the publisher's record gives it; the site's reference prints 224–230); the paper is held on the source card. The page is dated to the issue month because the record gives no day.

Acceptance. The paper is a refereed journal publication, the refereed evidence. The site's curator, T. F. Bloom, marks the problem proved and credits Alon's bound on the problem's page at erdosproblems.com; that credit is the reviewed evidence. Two Lean formalizations of Alon's upper bound exist, both by others: one posted to the site's forum on 2026-05-08, written with the Aristotle system, and its copy in a public repository of Lean proofs of Erdős problems, whose header names Alon as the informal author. The site's Lean qualifier refers to them. This corpus has built neither, so the claim is not formalized.