VibeMathedMath problems solved with AI
Sign in

Nonquadraticity of Lambert series values and improved bounds for Erdős Problem 1049

Erdős problem #1049 · erdosproblems.com/1049

Let t>1t>1 be a rational number. Is ∑n≥11tn−1=∑n≥1τ(n)tn\sum_{n\ge1}\frac{1}{t^n-1}=\sum_{n\ge1}\frac{\tau(n)}{t^n} irrational, where τ(n)\tau(n) counts the divisors of nn? A conjecture of Chowla; Erdős (1948) proved it for every integer t≥2t\ge2.

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
Irrationality and algebraic degree
Posed by
Chowla (conjecture); Erdős, Problem 1049 (Er88c, p. 102)
Year posed
1988
Years open
38y
Solved
2026-10-07
Model
Generative AI, model not named in the source (submitter: GPT-6 Astra via OpenAI Codex)
Vendor
OpenAI
Collaborators
Costa Lambrinoudis
Verification
Lean-checked, statement unaudited
Publication
Announced
Significance
12 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For rational bases t=a/b>1t=a/b>1, F(t)=∑n≥1(tn−1)−1F(t)=\sum_{n\ge1}(t^n-1)^{-1} is irrational whenever log⁡b/log⁡a<0.5728\log b/\log a<0.5728, and a formalized refinement reaches 0.5732900.573290. The previous thresholds were 1/2−1/π2≈0.39871/2-1/\pi^2\approx0.3987 (Bundschuh and Väänänen, 1994) and 0.4056830.405683 (W. Cook, September 2026, self-published). Problem 1049 itself stays open: t=3/2t=3/2, with log⁡2/log⁡3≈0.631\log2/\log3\approx0.631, is still outside the region.

Along the way, for every integer q≥2q\ge2 the numbers 1,F(q),F(q)21,F(q),F(q)^2 are linearly independent over Q\mathbb Q, so the Erdős-Borwein constant F(2)F(2) is not quadratic irrational. Both follow from one degree criterion for real algebraic bases: no relation of degree at most ee over Q(q)\mathbb Q(q) when eλlog⁡M(q)<log⁡qe\lambda\log M(q)<\log q, with λ=(42963+428220/π2)/202140≈0.42718\lambda=(42963+428220/\pi^2)/202140\approx0.42718.

What the AI did

The repository README says generative AI performed nearly all of the mathematical work: it developed the determinant construction and the algebraic-degree arguments, conducted the literature search, wrote the manuscript and produced the Lean formalization, with Costa Lambrinoudis directing and supervising. The manuscript's footnote says the same and names no model; the model and the use of OpenAI Codex are the submitter's account.

Verification

No independent mathematician has checked this yet. Read by this site on 15 October 2026, not rebuilt. The Lean development (Lean 4.33.1, mathlib, about 200 files at commit 008e313) has no sorry, admit, axiom declarations, native_decide or implemented_by in the library; the one unsafe def is the optional kernel-replay script under verification/, outside the library. lambertValue is the series ∑n≥01/(qn+1−1)\sum_{n\ge0}1/(q^{n+1}-1), faithful to the problem. The headline statements were read: lambertValue_irrational_of_log_ratio_lt_5728 and lambertValue_irrational_of_certified_region (any integers 0<b<a0<b<a with log⁡b/log⁡a\log b/\log a below 0.5728 or 0.573290) and erdosBorwein_no_quadratic_relation; they carry no extra hypotheses. The repository's axiom audit allows only propext, Classical.choice and Quot.sound; there is no CI and the build was not reproduced here. The refinement certificate generator was re-run here: 400 cells regenerated, Lean data file matches byte for byte, 4 unit tests pass. Arithmetic redone here confirms 1−λ=0.5728171-\lambda=0.572817, 2λ=0.8542\lambda=0.854 and the refined cutoff 0.5732901. Not Lean-verified: Formal Conjectures has Erdős 1049 (open) and its integer-base variant, but no statement of either result. Self-published, unrefereed.

Sources

Submitted by CobaltMongoose239 on

Changelog2 changes

Discussion