Erdős problem 358

When $A_n = n$ , the function $f$ defined above counts the number of odd divisors of $n$ .

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/358.lean

Formal Conjectures

FormalConjectures/ErdosProblems/358.leanErdos358.erdos_358.parts.i1 lineExact file

1True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop

SolvedStatement only, no proof

Reported by these sources. Not reviewed here.

AI collaborating with humans
Erdős AI contributions wiki · 13-20 Feb, 2026
Machine
GPT-5.2 Thinking
People
Nat Sothanaphan
Open the source record
AI standalone
Erdős AI contributions wiki · 11 Feb, 2026
Machine
GPT-5.2 Pro
Open the source record