qedbot

Erdős·erdos:684

Erdős 684

problem formal record: unclassified source: open F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

A Palomar registration names this problem. It is shown below but not counted as a check of the claim.

Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

number theory, primes, binomial coefficients·Source

AI activity

How grades work
OpenAI internal model

31 Mar 2026

Partial result

partial A3 V1 F2
Reasoning and sources

Autonomy

AI standalone; human involvement recorded as non-significant

GPT-5.2 Thinking

19 Jan 2026·with Quanyu Tang

Partial result

partial A1 V1 F2
Reasoning and sources

Autonomy

AI collaborating with humans

GPT-5.4 Thinking

2 Apr 2026·with Nat Sothanaphan

Partial result

partial A1 V1 F2
Reasoning and sources

Autonomy

AI collaborating with humans

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

declares divergences from its source reviewed by its authors only

Checks

1
  • verified·Palomar

    Registered by Palomar at 4543ff77: Comparator confirmed 5 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

    project registered at a pinned commit·2026-09-03·commit 4543ff7764f9

    PALOMAR-2026-09-03-000006 — names this problem; not counted as a check of the claim

Declared by the projects

1

As each project's formalization.yaml states it.

Erdős Problem 684: f(n)/log n is unbounded — a Lean 4 formalization of arXiv:2604.23784jidodat/erdos684-lean · joined by names · Palomar

Read formalization.yaml

authors
Ji Ho Bae
method
agent
review
self-assessed (Ji Ho Bae)
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
3 main results named, checked with Comparator, with an alignment table
sources
Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling — formalizes, authors participated; Erdős Problem #684 (erdosproblems.com) — background; Some unconventional problems in number theory — background; Short proofs in combinatorics and number theory — background
related
AlexKontorovich/PrimeNumberTheoremAnd — builds-on
divergences
The formal statements are those of the paper (Theorem 1.2, displays (4) and (5)), with f(n) valued in ℕ∞ so that the paper's convention f(n) = +∞ for an empty defining set is literal. The proof differs from the paper's text in simplifications only, all recorded in the README: in Lemma 3.1 only the upper bound is needed and it is obtained from θ(K) ≤ (1+o(1))K and the monotonicity of x ↦ 1 − log h/log x instead of partial summation, so that the Mertens-type sum (10) of the paper is not used; ψ(x) − θ(x) = O(√x) is replaced by Mathlib's ψ(x) − θ(x) ≤ 2√x log x; the prefix extraction in Step 3 of Lemma 4.1 is an abstract lemma proved by induction on the total depth; the decomposition into the ranges (I)–(IV) carries the hypothesis M ≤ K, which the paper uses implicitly; and the prime number theorem enters as θ(x) = x + O(x/log² x), weaker than the remainder (8) quoted in the paper, and is derived from PrimeNumberTheoremAnd's MediumPNT rather than cited.
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 0

No formal statement located.

Cited proofs · 0

No proof artifact cited by the formal record.

Recorded elsewhere

Compare the registries
  • palomar — Erdős Problem 684: f(n)/log n is unbounded — a Lean 4 formalization of arXiv:2604.23784

    checked·their labels: registered

  • vibemathed — Erdős Problem #684

    contested·their labels: contested

Also known as · 1
  • https://www.erdosproblems.com/684

Cite this record

qed.bot, “Erdős 684”, https://qed.bot/s/erdos-684, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.