VibeMathedMath problems solved with AI

Transcendence in the affine case of Erdős Problem 270

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

For integers a1a\geq1 and b1ab\geq1-a, the series Ca,b=n=1n!/((a+1)n+b)!C_{a,b}=\sum_{n=1}^{\infty} n!/((a+1)n+b)! is transcendental. Equivalently, the series in Erdős Problem 270 is transcendental whenever f(n)=an+bf(n)=an+b is a positive integer-valued affine function.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Transcendence theory
Posed by
Paul Erdős and Ronald Graham
Year posed
1980
Years open
46y
Solved
2026-08-22
Model
GPT-5.6 Sol (Codex)
Vendor
OpenAI
Collaborators
Verification
Unreviewed
Publication
Announced
Significance
12 / 100
Disclosed cost
Wikipedia
No dedicated article

What was actually shown

The manuscript claims Ca,bC_{a,b} is transcendental for every a1a\ge1 and b1ab\ge1-a, settling the positive integer-valued affine subclass of Erdős Problem 270. Two pieces of context matter. Problem 270 as Erdős and Graham posed it, for every f(n)f(n)\to\infty, was already answered no by Crmarić and Kovač in 2025: for any α>0\alpha>0 some such ff makes the series sum to α\alpha. What survives is the non-decreasing case, and the affine family sits inside it. Separately, the checkable parts here were already known - the short irrationality proof for C1,0C_{1,0} is Crmarić and Kovač's, posted by Kovač on the Erdős Problems forum in July 2026 and credited in the repository, and base-case transcendence follows a 2023 MathOverflow argument. The new content is the extension to the whole affine family, which is the part with neither formalization nor review.

What the AI did

The author's account, given to this site on submission rather than in the manuscript: OpenAI Codex independently rediscovered the elementary denominator argument, connected Crmarić and Kovač's Gaussian integral representation with a MathOverflow Siegel-Shidlovsky argument to obtain base-case transcendence, and developed the claimed extension to all positive affine cases using hypergeometric E-functions, Euler-operator reductions and a formal-at-infinity resonance argument. It located the relevant results of Salikhov, Salikhov-Viskina and Beukers, drafted the manuscript, and produced most of the Lean formalization; further AI reviews identified gaps and prompted revisions. The manuscript's own disclosure is a single line - "This manuscript was written and checked using generative AI" - which names no model and describes only writing and checking. The tier here follows the detailed account because the submitter is the author, but a reader following the source link will not find it there.

Verification

Read here on 24 August 2026 at github.com/clambro/erdos-270-transcendence. The elementary irrationality theorem for a1a\ge1, 0ba0\le b\le a is unconditional, and the five proof modules total 977 lines with no sorry, no admit, no declared axiom and no native_decide on Lean 4.33.1. The general transcendence theorem is not formalized. Salikhov, Salikhov-Viskina, Beukers, the Levelt-Turrittin decomposition and the step from the resonance calculation to functional minimality are passed as explicit Lean hypotheses rather than hidden behind axiom declarations, which is the honest construction; but for the novel range b>ab>a the hypothesis BeyondStripInput.pair is the conclusion itself, so the formalization lends the new claim no independent weight. Lean was not compiled here. The manuscript is unrefereed, self-published in a GitHub repository, and two days old at review.

Sources

Submitted by CobaltMongoose239 on

Changelog2 changes

Discussion