Is there an absolute constant such that, for every , if is sufficiently large then has at most divisors in .
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
FormalConjectures/ErdosProblems/887.leanFormal Conjectures
1∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ sorryNative pull-request state, mechanical checks, semantic findings, and artifact availability are separate source facts. None is a Vela Verification, Decision, or change to Math Standing.
Formal Conjectures PR #1237
answer slot scope fidelity
At exact PR 1237 head 28860856/blob 6feb58b9, the docstring asks for one absolute K, but answer(sorry) occurs under the C and n binders.
Witness: For each bound instance the answer slot can take the left-hand divisor count, and le_refl closes that instance; the slot therefore does not choose one absolute K.
Limit: The clean-candidate ground-truth exit still requires a separate independent-human fidelity pass. The witness is exact-head and does not rely on later Erdős 887 rewrites.
lean build
The exact PR head completed the repository Build project job successfully.
Limit: A successful build does not establish answer-slot scope fidelity.
Read-only projection
Approval and merge remain upstream PR state. A passing build does not establish semantic fidelity. An unavailable artifact identity is not a proof failure.
Adapter conformance 9 / 9: exact source revision, bounded complete reads, typed roots, custody, implementation identity, reconstructibility, unsupported-state refusal, rights, and lifecycle semantics.
Find a Problem, Result, source, or page