---

Claim. For an integer $q>1$ and a nonzero rational $r$ with $r\ne q^m$ for every $m\ge1$,

$$\sum_{n=1}^{\infty}\frac1{q^n-r}$$

is irrational (Theorem 4 of the paper, in its sign convention; equivalently $\sum_{n\ge1}(q^n+r)^{-1}$ is irrational for nonzero rational $r\ne-q^m$). With $q=2$ and $r=3$, which is no power of $2$, the series $\sum_{n\ge1}1/(2^n-3)$ is irrational, answering Problem 1050 yes. The paper is Peter B. Borwein, On the irrationality of $\sum(1/(q^n+r))$, J. Number Theory 37 (1991), no. 3, 253--259, received 1987-05-25, revised 1989-10-09 and published in the March 1991 issue (the page's date); its introduction names the series $\sum1/(2^n-3)$, which Erdős and Graham had listed as unresolved, as a special case. The card borwein_1991_irrationality_1_qn_r summarizes the argument: Padé approximants to the $q$-logarithm $L_q^*(x)=\sum_{m\ge1}x/(q^m-x)$, whose denominators have integer coefficients and controlled growth, are combined with the dilation identity $L_q^*(qx)=L_q^*(x)+x/(1-x)$ and a clearing factor to produce nonzero integer linear forms in $1$ and $L_q^*(r)$ that tend to zero, which rationality of $L_q^*(r)=r\sum_{n\ge1}(q^n-r)^{-1}$ forbids. A remark of the paper adds that the value is not a Liouville number. Borwein gave a second, self-contained proof in On the irrationality of certain series, Math. Proc. Cambridge Philos. Soc. 112 (1992), no. 1, 141--146, received 1991-11-12 and published in the July 1992 issue (the date of the second paper link): its Theorem 1 proves $\sum_{n\ge1}1/(q^n+r)$ irrational for every integer $|q|>1$ and nonzero rational $r\ne-q^n$ by a contour-integral argument, and its introduction says that the 1991 paper resolved the series $\sum1/(2^n-3)$; the card borwein_1992_irrationality_certain_series summarizes the argument. The classical case $q=2$, $r=1$ is Erdős's 1948 theorem that $\sum1/(2^n-1)$ is irrational (card erdos_1948).

Acceptance. The refereed evidence is the journal publications cited above. The reviewed evidence is the documented acceptance by the catalog erdosproblems.com, whose page for the problem (the discussion link) carries the label PROVED, last edited 2025-09-29, and whose curator, Thomas Bloom, credits Borwein with the proof, in the general form stated above (accessed 2026-09-04; the site's thread had no posts). As of 2026-10-06 the community database behind the site records the status as proved with a Lean qualifier, resting on the third-party development described below. No independent check of the paper's argument is recorded.

Formalization. A third party formalized the result: erdos_1050 in LeanGallery/NumberTheory/Erdos1050/Statement.lean of https://github.com/gotrevor/lean-gallery, pinned above at the commit of 2026-07-05 that last touched the folder. The file names Trevor Morris as its author and Borwein's 1991 paper, beside the 1992 paper, as the resolving theorem it formalizes, specialized to $q=2$, $r=-3$, so it is a link on this page rather than an independent claim; the formal-conjectures catalog describes the development as formalized by Trevor Morris with Claude Code and Harmonic's Aristotle. Its theorem states that $\sum_{n\ge0}1/(2^{n+1}-3)$ is irrational, the problem's series reindexed from $n\ge1$; the file says the proof reduces the literal series to the tail $\sum_{n\ge0}1/(2^{n+2}-3)$ by discarding the rational first term $-1$, and that its axioms should be only propext, Classical.choice and Quot.sound. The catalog (the record link, pinned to the commit of 2026-09-18 that last touched its file) tags its statement erdos_1050 as research solved and cites this file as the formal proof, together with the development's proofs of Borwein's general theorem and of Erdős's 1948 case as variants. No build of the development, printout of its axioms or audit of its definitions against the problem is recorded in this repository, so the claim carries no formalized evidence and the file's own account of its axioms is reported, not warranted.

Depends on. Nothing in this wiki.