Skip to content

Erdős problem 887

Is there an absolute constant KK such that, for every C>0C > 0, if nn is sufficiently large then nn has at most KK divisors in (n12,n12+Cn14)(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}}).

Result history

Published changes, performers, checks, and later corrections.

No result history yet
No proposed change is retained for this Problem, so there is nothing to show a decision on.

Correction history

No correction history

Technical detailsExact roots, source, and retained record identifiers

Exact provenance

Problem row
sha256:b7751274d3496049a00a81e9a2b734c7ad0dda2dcf62838666b751842b35c090
Metadata
sha256:1f1f8d783521e857f5f69d133c8dfbb851fcf9e236b36d9b16abe923641a0f2e
Observation
sha256:8c823d621b7e1256c8e47c60a5f1c54c016a5507e6f27b2bab537f6f5f232067
Content
sha256:8ae5ccd492573a8b21cc9278213c08521a2f11142794fac4ab22f0c315d0c29c
Repository
sha256:a956b84c437202e5a02cc9e036a621bd14a302b34a75758115730bdbb77c52a4
Projection
sha256:c9d14c459c518937e758918b5897dc3b22f1a55f07739afe99502f5b046c907a
Source commit
2415f78e850aeee50afdca525c6f2e0ea606f207
Upstream sourceInspect recordsSource JSON

Source review

1 exact matching record

Native 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

FormalConjectures/ErdosProblems/887.lean

PR mergedreview approvedsource audit: needs revision
failsemantic

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.

passmechanical

lean build

The exact PR head completed the repository Build project job successfully.

Limit: A successful build does not establish answer-slot scope fidelity.

Open upstream PROpen Problem 887head 288608562e

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.

Web read projection
sha256:ca753f3b6ad07fd62ef1035ae56de1646cb2133dd1705f991bf29a2bd7da2780
Math source projection
sha256:1a90cbe1732e21e730753a12e6b3b1ecbd3e0019a287a5ba001c9a9fdccf881b
Adapter profile
sha256:6491df603d880f00dc7e69cb0817fda1a0d903efee3812c5af3c7b3e02773303
Adapter contract
sha256:5de25828202d0682f8ac39c2e58e5d9ed7a3f0474910d77c1c4e641a08543615
Inspect exact Math projection
View complete five-record source audit

Search problems.science

Find a Problem, Result, source, or page