Transcendence in the affine case of Erdős Problem 270
Erdős problem #270 · erdosproblems.com/270
For integers and , the series is transcendental. Equivalently, the series in Erdős Problem 270 is transcendental whenever 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 is transcendental for every and , 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 , was already answered no by Crmarić and Kovač in 2025: for any some such makes the series sum to . 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 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 , 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 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