Erdős·erdos:684
Erdős 684
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 workPartial result
Reasoning and sources
Autonomy
AI standalone; human involvement recorded as non-significant
Sources
Partial result
Reasoning and sources
Autonomy
AI collaborating with humans
Sources
Partial result
Reasoning and sources
Autonomy
AI collaborating with humans
Sources
Does the formal statement say what was claimed?
F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
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
Declared by the projects
1Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.
Erdős Problem 684: f(n)/log n is unbounded — a Lean 4 formalization of arXiv:2604.23784
- 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 discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
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
- vibemathed — Erdős Problem #684
Also known as · 1
- https://www.erdosproblems.com/684