— saved image
Costa @Clambr0 [Follow]
hello Erdős asked if Σ n!/(2n)! is irrational
It is. Five-line proof. Extends to the whole family Σ n!/((a+1)n+b)! for a≥1, 0≤b≤a. Lean verified.
My AI then went crazy and claimed the whole affine family a≥1, b≥1-a is transcendental using techniques beyond my understanding:
[link card]
clambro/erdos-270-transcendence
Transcendence in the Affine Case of Erdős Problem 270
1 contributor · 0 issues · 0 stars · 0 forks
GitHub - clambro/erdos-270-transcendence: Transcendenc...
From github.com
2:26 PM · Aug 22, 2026 · 71.2K Views
10 replies · 30 reposts · 465 likes · 193 bookmarks
Relevant ▾ View quotes >
[next post in thread]
Costa @Clambr0 · Aug 22
[embedded image of typeset math, bottom partly covered by phone nav bar]
Let
C = Σ_{n=1}^∞ n!/(2n)! = Σ_{n=1}^∞ 1/D_n, D_n := (2n)!/n!.
Since
D_{n+1}/D_n = 4n + 2 ∈ ℤ,
we have D_n | D_{n+1}.
Let P_N = Σ_{n≤N} 1/D_n and R_N = C − P_N. Then D_N P_N ∈ ℤ, while
0 < D_N R_N ≤ Σ_{k≥1} 1/(4N+2)^k = 1/(4N+1) → 0.Note from Claude Sonnet 5
Tweet by Costa (@Clambr0) saying a five-line, Lean-verified proof shows the Erdős-asked series sum of n!/(2n)! is irrational (extended to a family), and that his AI then claimed transcendence for a wider affine family, linking a GitHub repo for Erdős Problem 270; below, the start of the thread with the typeset irrationality proof. Posted 2026-08-22.
mathematicserdos problemsirrationalitytranscendenceleanai math resultsformal verification