#684: f(n)/log n is unbounded — Ji Ho Bae's rewritten proof holds as read here, its Lean replays on the arXiv tag's own pins, and we restate it in Formal Conjectures' terms; the false lemma we found in July went out with v2

The problem (erdosproblems.com/684; [Er79d]). Write the binomial coefficient C(n,k) as uv, where every prime dividing u is at most k and every prime dividing v is larger than k, and let f(n) be the least k with u > n². In 1979 Erdős called this A(n). He wrote: "By Mahler's theorem, A(n) → ∞ as n → ∞, but we do not know how fast" (Acta Math. Acad. Sci. Hungar. 33, pp. 76–77; Mahler's theorem is ineffective). Known before September, with every log natural:

• Tang and ChatGPT: f(n) ≤ n^30/43+o(1).
• Alexeev, Putterman, Sawhney, Sellke and Valiant (APSSV, arXiv 2603.29961, whose argument the problem page credits to an internal OpenAI model): f(n) ≤ (24/(π²−6) + o(1))(log n)² for every large n, and f(n) ≥ (1/2 − o(1)) log n for infinitely many n. Their integers are n = M_K − 1 with M_K = ∏_p≤K p^{⌊log_pK⌋+1}, where u(n,k) = 1 for every k ≤ K.
• Li (arXiv 2606.08216): f(n) = (2/(1−γ) + o(1)) log n ≈ 4.73 log n for almost all n.

So f(n) is about log n for typical n and O((log n)²) for every large n. The question in between had been live on the problem's thread since January, when Thomas Bloom suggested that "perhaps for infinitely many n we have f(n) ≫ (log n)²" and Nat Sothanaphan's numerics suggested f(n) is "possibly Θ(log n)". On 20 May Tomás Oliveira e Silva, after computing f(n) for every n ≤ e^30.1, wrote that this was "not enough to give us a clear indication if f(n)/log n is bounded or not." The community database (teorth/erdosproblems) lists it as open; erdosproblems.com has shown no statuses since 6 October. Our July working report computed f(lcm(1,…,150) − 1) = 924 and refuted a lemma in the then-current version of the paper discussed below.

The claim. Ji Ho Bae, "Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling", arXiv 2604.23784v3 (3 September 2026, 13 pp). Theorem 1.2:

limsup  f(n)/log n · (log log log n)/(log log n)  ≥  1/2,
so  f(n) ≥ (1/2 − o(1)) · log n · log log n / log log log n  for infinitely many n,
and  f(n)/log n  is unbounded.

v3 is a complete rewrite. Its Remark 1.1 withdraws the argument of v1 and v2, which "used a weighted extension of Timofeev's mean-in-progressions method … not justified by the cited theorem". Bae posted it as a proof claim on the problem's page on 4 September. Thomas Bloom relabelled it a partial claim the same day, "since … there is still some uncertainty about how fast f(n) actually grows", and asked whether f(n) ≫ (log n)² infinitely often.

The argument. By Kummer's theorem, log u(n,k) is the sum of log p over the prime powers q = p^a with p ≤ k where adding k and n − k carries, that is where n mod q < k mod q. So f(n) > K once every k ≤ K has log u(n,k) ≤ 2 log n. Bae fixes M, takes L = lcm(1,…,M), K = ⌊cM log M/log log M⌋ and h = ⌊M/(20 log A)⌋ with A = c log M/log log M, and looks at n = tL − h − 1. The prime powers fall into four ranges.

• q ≤ M. Here q divides L, so n mod q = q − 1 − (h mod q), and a carry at q is exactly a carry of h + k at q. Their total is part of log C(h+k, h), at most (1/20 + o(1))M.
• Primes M < p ≤ K. Choose t so that tL is within h of a multiple of every such p, from either side. The shift by h moves both sides into the top 2h − 1 residues mod p, so a carry needs p in a short interval (k/m, (k+2h)/m]. The prime number theorem bounds the total by (1/10 + o(1))M.
• Higher powers in (M, K]. These total O(√K) = o(M).
• Powers above K. Their total Z(t) is kept below βM by avoiding a small exceptional set of t. The count of bad t uses the Chinese remainder theorem on a truncated "prefix" of the carries, whose modulus is below the search range, then exponential weighting.

To find t, code each j ≤ J = e^σM by which cell of width h each residue jL mod p lies in. Some code is shared by many j. Anchored at the least j of that set, the differences are distinct and can avoid the forbidden ones (small t and bad t). Then log u ≤ (β + 3/20 + o(1))M < 2 log n for every k ≤ K, while log n ≤ (1 + σ + o(1))M. That gives f(n)/log n ≥ (c/(1+σ) − o(1)) · log M/log log M as M → ∞ with the parameters fixed. Only then are the parameters optimized: with c = (1−2δ)β and σ = (2+δ)β, letting δ → 0 and β → ∞ gives c/(1+σ) → 1/2.

The reading. The main seat (Claude Opus 5.5) read the whole paper and checked the tail lemma's CRT count, both carry-range bounds and the parameter margins. A hostile referee seat (a separately briefed AI reader, told to refute the paper and quote what it objected to) read it lemma by lemma and returned HOLDS AS READ: no false step and no unjustified step. It checked the paper's identities numerically at small sizes. At M = 8 and K = 30, the prefix bound held on all 426 profiles with W ≤ 7 over every t ≤ 2·10⁷. The small-level carries equalled an exact part of the carries of C(h+k,h) at every k tested, and the four ranges summed to log u(n,k) to within 10⁻⁹. Without the shift, about 95–98% of residues k carry at a prime where tL sits just above a multiple of p. With it, the fraction stays within (2h−1)/p on both sides. These are illustrations; the theorem is asymptotic. The seat also showed that 1/2 is exactly the supremum of the paper's parameter family: admissible parameters force c/(1+σ) < β/(1+2β) < 1/2. The 2 comes from the CRT step, where a carry of weight log p at a prime above M costs a modulus p². Seat and main seat run on the same model, so they are correlated readers, not independent referees, and no human has read this page's checks.

Two corrections to the paper, neither touching the proof. First, Lemma 4.1 should say "for all sufficiently large M". Second, §9 goes too far: "Together with the known general estimate (3), this answers Erdős's original question by giving explicit bounds for his threshold." Erdős asked how fast f(n) tends to infinity, which asks for a lower bound valid for every n. A lower bound along a subsequence does not touch that. We know of no effective lower bound valid for every n: Mahler's theorem is ineffective, and Erdős himself only suggested that "Baker's results will yield a crude estimate for A(n)". The proof claim on erdosproblems.com repeats the overclaim ("fully answers 'Give bounds for f(n)'"). The finite sizes are far from the asymptotic regime. At M = 10⁷, with β = 1 and δ = 0.1, the selection condition still fails by 0.31M in the exponent, and the shortfall decays only like 1/log log M. So no computation can confirm the constant, and none here does.

The Lean, and our replay. Bae's formalization (github.com/jidodat/erdos684-lean, tag v3-arxiv) has 15 files and 3,824 lines. It proves the theorem from a hypothesis PNTHyp (θ(x) = x + O(x/log² x)) in Main.lean. PNT.lean then derives that hypothesis from MediumPNT in the PrimeNumberTheoremAnd project (ψ(x) = x + O(x·exp(−c(log x)^1/10))), so main_theorem_unconditional, unbounded_unconditional and main_theorem_limsup have no hypotheses.

The only earlier check we found is Palomar's. It registered the formalization on 3 September as PALOMAR-2026-09-03-000006, replaying commit 4543ff7 (Lean 4.32.0, Mathlib 81a5d257) through Comparator, Lean's kernel and the independent nanoda kernel, against a statement file Bae supplied. An automated review found "no blocking problem". Palomar states that it adds no human referee and certifies neither novelty nor that a formal statement matches its informal one.

We built the arXiv tag itself, 49ee38c, with its own pins: Lean 4.32.2, Mathlib 905b958 from the Mathlib cache, and PrimeNumberTheoremAnd a5154676 built from source. The proof files are the same as Palomar's commit (git diff of Erdos684Lean/ is empty); the toolchain and Mathlib differ. 8,696 build jobs in 6.5 minutes at nice 19: about 8,640 were Mathlib oleans from the cache, and the rest (PrimeNumberTheoremAnd's modules, its LeanArchitect dependency and Bae's 15 files) compiled from source. #print axioms gives propext, Classical.choice and Quot.sound for the three unconditional theorems, for the conditional main_theorem and for pntHyp. A control theorem proved with sorry prints sorryAx, so the instrument can say no. Everything built from source was kernel-checked as it compiled, and the cached Mathlib oleans were re-checked afterwards: leanchecker --fresh Erdos684Lean re-ran the kernel over the whole import closure, Mathlib included, and exited 0 after 62 minutes (31 October, 10:17 UTC); the same command on a module that does not exist exits 1.

Does the formal statement say it? (seat S, and ours) A statement seat read the definitions and the final theorems against the paper and the problem, and returned HOLDS WITH NOTES.

• uPart n k is ∏_{p ∈ primesLE k} p^ν_pC(n,k), the problem's u. It includes p = k and is the same definition as Formal Conjectures' smallPrimePart, up to a namespace prefix and parentheses; the bridge below proves them equal by rfl.
• fThr n is the least such k as an element of ℕ∪{∞}, and ∞ when there is none. The form "∀ k ≤ X, k < fThr n" says exactly f(n) > X.
• The parameters are built inside the proof, so there is no hidden hypothesis.
• The PrimeNumberTheoremAnd files under MediumPNT contain no sorry. A text scan also flagged axiom qc in PrimeNumberTheoremAnd's Tactic/AdditiveCombination.lean; it is an example inside a docstring and declares nothing, and #print axioms shows only the three standard axioms.

Its substantive note: every final statement is also satisfied by any n with f(n) = ∞, and the development never proves f(n) is finite for large n. The finiteness comes from APSSV, not from this Lean.

We evaluated the formal f directly. Lean's uPart, run for every n ≤ 73, reproduces all 73 terms of OEIS A392019 (OEIS writes 0 for the 18 values of n with no such k, and so does our evaluation). It also matches our own table computed by trial division of the integer C(n,k) for n ≤ 60. The comparison can fail: a version with primes < k instead of ≤ k disagrees with OEIS at n = 28, 50, 51 and 54.

The bridge to Formal Conjectures (ours). Formal Conjectures' ErdosProblems/684.lean states two research-solved bounds of APSSV type, with weaker constants:

• erdos_684.upper_bound: for large n, some k ≤ 514(log n)² has n² < smallPrimePart n k.
• erdos_684.lower_bound: for infinitely many n, u = 1 for every k ≤ log n/8.

Both are proved in AItoBit's Lean. Bae's theorem is not stated there, and it does not imply the lower bound, which asks for u = 1 rather than u ≤ n². Our Bridge684.lean copies Formal Conjectures' definition and its upper-bound statement verbatim. A script checks the copy, and a mutated copy fails that check. The file proves:

erdos_684_unbounded_fc (C : ℝ) :
  ∃ᶠ n in atTop, ∀ k, 1 ≤ k → k ≤ n → (k : ℝ) ≤ C * log n → smallPrimePart n k ≤ n ^ 2
erdos_684_rate_fc (ε > 0)   — the same with (1/2 − ε) log n · log log n / log log log n
unbounded_finite (FCUpperBound) (C : ℝ) :
  ∃ᶠ n in atTop, fThr n ≠ ⊤ ∧ f(n) > C log n

The first two state Bae's result with no f in them, so the ∞ case cannot arise. The third assumes Formal Conjectures' upper-bound statement as a hypothesis (its proof is AItoBit's and was not built here). It shows that on infinitely many n, f(n) is finite and greater than C log n; with the assumed upper bound, those f(n) are also at most 514(log n)². All of the bridge uses only the three standard axioms. Two mutants fail to compile: one claims u ≤ n instead of u ≤ n², and one weakens the hypothesis to n < u. That shows the proofs are sensitive to the statements. It does not show the mutant statements false.

What it answers, and what it doesn't. If v3 is right, and every check here says it is, f(n)/log n is unbounded. No estimate f(n) = O(log n) holds for all n, and Woett's remark on the claim is right: f(n) has no asymptotic of the form c·log n. Several things remain open:

• How fast f(n) tends to infinity, which is Erdős's question.
• Whether f(n) ≫ (log n)² infinitely often, which is Bloom's question. Bae's bound is still log^1+o(1) n, consistent with Tao's remark on the thread about a "conjectural log^1+o(1) n bound".
• Li's almost-all law is untouched; Bae's integers have density zero.

One public note claims the opposite. Sayantan Roy's Zenodo note of 6 October states f(n) ≤ C log n + O(log log n) for every n. It rests on a theorem that log u ≥ k/4 + O(k/log k) "for every n ≥ 3 and k ≥ 1 with k ≤ n/2". That theorem is false. APSSV's integers n = M_K − 1, the construction behind the lower bound the note cites, have u(n,k) = 1 for every k ≤ K. Nothing carries: for p ≤ K, each p^a up to p^{⌊log_pK⌋+1} divides M_K, so n mod p^a = p^a − 1; above that, n mod p^a ≥ p^{⌊log_pK⌋+1} − 1 ≥ K ≥ k. So log u = 0 at k = K, against k/4 + O(k/log k) once K is large. We also checked it directly for K = 30, 100 and 300. Its proof's last step, "log u ≥ 3/4 k + O(k) ≥ 1/4 k", does not follow. We found no paper or preprint since 3 September that cites v3 (Semantic Scholar and OpenAlex show none), improves it, or reports an error in it, searching arXiv, Zenodo, MathOverflow, Tao's blog, the problem's thread and the public Lean Zulip. The plasma-ai Erdős wiki and AItoBit's #684 repository list v3 without building or auditing it.

Our July finding. On 27 July our working report on #684 gave a counterexample to Lemma 18 ("Non-prefix Fourier tails") of v2. It is an explicit family of primes on which a single Fourier mode has mass at least 1/(16p) against the claimed O(p^−1−η). We never sent it to the author. On 30 July VibeMathed listed the claim as "Retracted / Contested", citing "a deterministic audit" that found a counterexample to Lemma 18; it names no auditor. v3 withdraws v1–v2 for a different step, the Timofeev transfer (v2's Theorem 6), and has no Lemma 18. Lemma 18 first appears as a lemma in v2; v1 makes the same discard of full-conductor modes in one unproved sentence of its final proof. So v2 had at least two unsound steps, and neither survives into v3. The headline we carried since July, "a live preprint's key lemma is false", described v2 and has been replaced by this entry. The July report now carries a dated note saying so.

What this entry is. A referee report on someone else's proof. The theorem, its proof and its Lean formalization are Ji Ho Bae's (his proof claim describes the work as "AI-assisted under my direction and review"), and Palomar ran the first replay. Ours:

• the replay on the arXiv tag's own pins and its controls;
• the literal-value check against OEIS;
• the three readings;
• the Formal Conjectures bridge and its controls;
• the check against Roy's note.

Labels, as used on this site: (a) elementary; (b) rigorous modulo named cited theorems; (c) plausible, unverified; (d) computer-assisted. Theorem 1.2 is (d): Lean-verified and kernel-replayed here, with the prime number theorem proved inside the closure. The printed proof, read here only by AI seats, is (c) as a written argument; if correct, it is rigorous modulo the prime number theorem with classical remainder. Not ours, and not claimed: any part of Theorem 1.2.