---

De Mathan proves, as Theorem 1 of his 1980 paper, that a sequence of monotonic differentiable functions on an interval whose consecutive derivative ratios lie between $\lambda$ and $\mu$, $1<\lambda\le\mu$, has a point $x$ at which its values are not everywhere dense modulo $1$, and that under a Lipschitz condition on the logarithms of the derivatives the set of such $x$ has Hausdorff dimension $1$. Corollary 1 specializes it to $q_nx$: for every sequence $(q_n)$ of positive reals with $q_{n+1}/q_n\ge\lambda>1$ and every interval $[a,b]$, the $x\in[a,b]$ for which $(q_nx)$ is not everywhere dense mod $1$ form a set of dimension $1$. The proof builds nested intervals whose common point $x$ has $\|q_nx\|\ge\varepsilon>0$ for all but finitely many $n$, and concludes (p. 241) that the $x$ for which $(q_nx)$ does not have $0$ as a point of accumulation mod 1 also form a set of Hausdorff dimension $1$.

For Problem 464 take $q_n=n_k$ and $\lambda=1+\epsilon$. That second set is uncountable, so it contains an irrational $\theta$; some $\varepsilon>0$ then has $|\theta n_k|\ge\varepsilon$ for all but finitely many $k$, and the finitely many excepted terms still have $\|\theta n_k\|>0$, so $\inf_k\|\theta n_k\|>0$ and $(\theta n_k)$ is not dense modulo $1$ (the problem page's two authored lines). That is the problem page's corrected Statement, the question as Erdős posed it; the site's wording, about the set of distances $\|\theta n_k\|$ in $[0,1]$, holds for every $\theta$ since $\|x\|\le1/2$ (the problem page's Notes). De Mathan states the question without the irrational clause and notes that the answer is obvious for $\lambda>2$. Pollington's independent solution has its own page; de Mathan's note added in proof on 8 April 1980 credits Pollington's paper, and Pollington's introduction credits de Mathan's.

The paper's library home is de Mathan 1980, with compiled pages for Theorem 1 and Corollary 1; the statements are taken first-hand from the paper, the existence part of the proof is followed and not checked, the dimension part for structure only, and nothing here is independently reviewed. De Mathan announced the result in a 1978 note, Sur un problème de densité modulo 1, C. R. Acad. Sci. Paris Sér. A 287 (1978), 277--279, cited by Pollington and linked above through its zbMATH record (Zbl 0393.10050); the note was not read.

Formalization. The statement file of the formal-conjectures project (FormalConjectures/ErdosProblems/464.lean) states the problem with the conclusion rendered as $(\theta n_k)$ not dense modulo one, marks it solved and points, through its formal_proof attribute, at the Lean 4 file in the repository Jayyhk/erdos-lean linked above at the pinned commit. That file proves erdos_464, the formal-conjectures statement, from its theorem deMathan_not_dense, an irrational $\theta$ whose distances $\|\theta a_k\|$ stay bounded away from $0$ along a lacunary sequence, obtaining irrationality from an uncountable set of admissible $\theta$; its docstrings name de Mathan's paper for the quantity $\|x\|$ and credit the solution to de Mathan and Pollington, and the site's thread comment of 21 June 2026 reports that the AI system Aristotle, given de Mathan's paper, formalized the argument of the first part of his Theorem 1. It is therefore recorded here as a formalization of this claim. The file contains no sorry and no axiom command at the pinned commit. This project has not built the file or audited its statement against the problem, so it supplies no formalized evidence; the site's label PROVED (LEAN) refers to this development.

Acceptance. The paper is refereed: B. de Mathan, Numbers contravening a condition in density modulo 1, Acta Math. Acad. Sci. Hungar. 36, no. 3--4 (September 1980), 237--241, received 28 November 1978. Erdős announced in 1982 that de Mathan and Pollington had settled the problem independently. The site's curator, Thomas F. Bloom, marks Problem 464 proved and credits this paper, with Pollington's, with the solution. The site credits this 1980 paper, and a credited source's date names its claim page, so the page is dated by the first day of the paper's issue month rather than by the 1978 note that announced the result.