Corpus.Erdos887.erdos_887.parts.ii
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^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})$.
Erdős Problem 887
formal-conjectures · erdos-problems · ams-11
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^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})$.
Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://www.erdosproblems.com/887
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/ErdosProblems/887.lean
Local target: Corpus.Erdos887.erdos_887.parts.ii
Source SHA-256: 39f1391b7b782f383f2a77eabcb93fb2de688319edc57aa519c3f6f556851bea
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Formal targets
Reusable lemmas
No public records on this page.
Public discussion
No public records on this page.