What was already known
Erdős and Graham asked whether the series S(f) is irrational for nondecreasing positive integer-valued f tending to infinity. Crmarić and Kovač showed that unrestricted f can give any positive real value and recorded the Gaussian integral form for the base case f(n)=n. Kovač later posted an elementary irrationality argument for that base case. A 2023 MathOverflow argument treated a related Gaussian integral using Siegel–Shidlovsky theory. Lambrinoudis reports that the affine-family extension was independently obtained by AI before learning of Kovač’s post (manuscript introduction, §§1–2).
AI involvement
Costa Lambrinoudis explicitly credits generative AI with nearly all mathematical work, including the affine extension and transcendence-theoretic arguments; Lambrinoudis directed and supervised the investigation. Christopher D. Long later suggested strengthening the earlier transcendence result to algebraic independence.
Costa Lambrinoudis explicitly credits generative AI with nearly all mathematical work, including the affine extension and transcendence arguments, while he directed and supervised the investigation. Christopher D. Long later suggested the algebraic-independence strengthening.
Importance
This settles the positive affine subfamily of Erdős Problem 270 much more strongly than irrationality, while the general nondecreasing-function question remains open.
Limitations
The claim covers only f(n)=an+b with integer a≥1 and b≥1−a. The published Lean development proves elementary irrationality and algebraic deductions, but leaves the analytic transcendence and algebraic-independence inputs unproved; thus it does not formally verify this main claim. No completed outside check of the full argument was located.
Technical verification
Lean verifies elementary irrationality and algebraic deductions from stated analytic inputs. The transcendence and algebraic-independence inputs required for this main claim are not proved in Lean, and no complete human check was documented.
- Supporting source (github.com) — Conditional proof modules and external input interface
Human understanding
Few is the default when evidence for a higher level is insufficient. The manuscript gives a proof outline, but it credits AI with writing the mathematical exposition; no named human is documented as explaining the central analytic independence argument.
Correction and publication history
Primary manuscript and formalization-scope review for non-notifying local inclusion.
Read this published revision