Is there an absolute constant $K$ such that, for every $C > 0$ , if $n$ is sufficiently large then $n$ has at most $K$ divisors in $(n^{1/2}, n^{1/2} + C n^{1/4})$ .

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

machinery: simultaneous-square-values,linear-forms-as-squares,bombieri-lang,lang-conjecture-integral-points,elliptic-integral-points,consecutive-integer-window,divisors-in-short-interval,intersection-of-conics,general-type-variety-finiteness

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

This is **open** in general [[nomath]](already open for $C=1$)[[/nomath]].

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_887.parts.i : ∀ C > (0 : ℝ), ∀ᶠ n in atTop,
    #{ d ∈ Ioo ⌊√n⌋₊ ⌈√n + C * n^((1 : ℝ) / 4)⌉₊ | d ∣ n } ≤ answer(sorry)

formal-conjectures/887.lean ↗

status

open

evidence

formal

status

Search Vela