For $0 \leq k \leq n$ write $(k n) = uv$ where the only primes dividing $u$ are in $[2, k]$ and the only primes dividing $v$ are in $(k, n]$ . Let $f (n)$ be the smallest $k$ such that $u > n^{2}$ . Give bounds for $f (n)$ .

Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

routes

witnesskummer_no_carry

extended no-carry witness table re-checked by the frozen verifier

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

f(M_K-1) > K verified for K=3..12 via Kummer no-carry (effective, subsequential lower bound)

targets

promote the subsequential bound to the full claim for all n.1

evidence

partial proof

machine-sealed

Erdos #684: verified effective subsequential lower bound f(n) >= (1/2+o(1)) log n. Explicit construction M_K = prod_{p<=K} p^{floor(log_p K)+1}; computationally verified (K=3..12) that all v_p(C(M_K-1,k))=0 for p<=k<=K (no Kummer carries), so the smooth part u=1 < n^2 for every k<=K, hence f(M_K-1) > K; with log M_K = psi(K)+theta(K) = (2+o(1))K this gives the stated bound along n=M_K-1. The pointwise lower bound f(n)->infinity is known only INEFFECTIVELY (Mahler); this effective statement is subsequential, not pointwise. UPPER side (GPT-Pro, not re-verified here): an elementary Kummer+Dusart argument gives f(n) = O((log n)^2). UNVERIFIED claims (cited preprints not confirmable from here, treat with caution): an 'APSSV' optimized constant 24/(pi^2-6) and a 'Bae 2026' limsup f(n)/log n = infinity.

{"construction":"M_K=prod_{p<=K}p^{floor(log_p K)+1}; f(M_K-1)>K","verified":"scripts/verify_684_construction.py (K=3..12)","effective_lower":"f(n) >= (1/2+o(1)) log n along n=M_K-1","pointwise_low...

depends on (the wall): scripts/verify_684_construction.py

scripts/verify_684_construction.py

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let [ \binom{n}{k}=u(n,k),v(n,k), ] where every prime factor of $u(n,k)$ is (\le k) and every prime factor of $v(n,k)$ is (>k). Equivalently, $u(n,k)$ is the “$k$-smooth part” of (\binom{n}{k}).

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

oeis

A392019 — If binomial(n,k) = u*v where the only primes dividing u are <= k and the only primes dividing v are > k, then a(n) is the least k such that u > n^2, or 0 if such a k doesn't exist.0,0,0,0,0,0,0,0,0,7,0,0,0,0,0,11,0,13,0,0,8,13,0,17,12,13,13,5,17,7,19,9,12,11,11,7,11,17,15,14,17,17,19,13,13,19,23,17,

links

have proved · paper

Create a formalisation here · link

status

open