---

Claim. The answer to Problem 964 is yes, and more is true. Sean Eberhard, Ratios of consecutive values of the divisor function, Journal of Number Theory 281 (2026), 426--428, first posted as arXiv:2505.00727 on 27 April 2025, proves that for every rational $q>0$ the equation

$$\frac{\tau(n+1)}{\tau(n)}=q$$

has infinitely many solutions $n$; density of the ratios in $(0,\infty)$ follows at once. The proof works with the set $R$ of ratios attained infinitely often. A special case of the Goldston--Graham--Pintz--Yıldırım sieve gives, for two of three linear forms $L_i(x)=a_ix+1$, infinitely many $x$ at which each $L_i(x)/r_i$ is a product of two distinct primes above a bound $C$. This puts one of three explicit divisor-count ratios in $R$. Replacing $r_i$ by $r_ip_i^{e_i-1}$ for suitable $e_i$ makes the three ratios equal, so their common value lies in $R$. A choice of prime blocks then puts in $R$ every finite product of the values $(x+1)(y+1)/(x+y+1)$ and their inverses, which is the subgroup they generate, and Eberhard shows that this subgroup is all of $\mathbb Q_{>0}$. A complete rewrite of the argument is on the main theorem page, and the sieve input is stated with its hypotheses on the Theorem 1 page of the source card. The sieve input is assumed at its published standing and is not reproved there.

Depends on. No page of this wiki.

Acceptance. Thomas Bloom, the site's curator, labels the problem proved and credits Eberhard's paper with the unconditional proof on the problem page; that credit is the reviewed evidence. The paper appeared in the Journal of Number Theory, the refereed evidence. The library card also records this corpus's own review of its rewrite of the proof; that review is not acceptance evidence here.

Formalization. Daniel Chin posted a Lean 4 file in the problem's discussion thread on 14 February 2026, written, as the post says, with the help of Aristotle and of Gemini through Antigravity, and asked for a check by someone experienced with Lean. The file declares itself a formalization of Eberhard's proof; its final theorem takes a formalized Goldston--Graham--Pintz--Yıldırım statement as a parameter, so it is a conditional formal proof of the argument downstream of the sieve. Terence Tao's response, moved to the site's formalization thread and quoted in the problem's thread the same day, found the file conditional on that statement and apparently correctly formalized. The site's label for the problem notes this Lean file. The link above is pinned to the repository commit of 14 February 2026 that last changed the file. The file declares no axiom and uses no sorry or admit; this corpus has not built it, so it is not listed as evidence.