Vela

Let be a rational number. Isirrational, where counts the divisors of ?

Worked, still open.

irrationality · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Write (t>1) and expand each term as a geometric series: [ \frac{1}{t^n-1}=\frac{t^{-n}}{1-t^{-n}}=\sum_{k\ge 1} t^{-nk}. ] Summing over (n\ge 1) and regrouping by $m=nk$ gives [ \sum_{n=1}^\infty \frac{1}{t^n-1} =\sum_{n=1}^\infty\sum_{k\ge 1} t^{-nk} =\sum_{m=1}^\infty \frac{|\\{(n,k):nk=m\\}|}{t^m} =\sum_{m=1}^\infty…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_1049 :
    answer(sorry) ↔ ∀ t : ℚ, t > 1 → Irrational (∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1))
formal-conjectures/1049.lean ↗

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 b922e3d5223f1a4e8163c8eba3cc2060c1d917e8f5a6872d85d20920aab1a6ca

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.