---

Claim. Let $f:\mathbb{N}\to\mathbb{R}$ be additive and let $D_f(X)=\#\{n\le X: f(n+1)<f(n)\}$. If $D_f(X)=o(X)$, then there is a constant $c\ge0$ with $f(n)=c\log n$ for every $n$. This is Theorem 1.1 of the manuscript Almost everywhere monotone additive functions, posted on Zenodo under the DOI linked above. The record was created on 2026-09-08 and states the publication date 2026-09-07; its version 2 was created the same day, its files were replaced on 2026-09-23, and it lists its creator as anonymous. This page describes the manuscript and archive of the 2026-09-23 revision. It answers Problem 1122 yes; that $c\ge0$ follows at once from the hypothesis, since $c<0$ would make $f$ decrease at every $n$. The site's proof-claims entry of 2026-09-08 names Qiyuan Gu as the claimant and says that GPT-6 Astra generated the proofs and drafted the manuscript, which the author reviewed. The manuscript's own declaration (p. 8) says that GPT-6 Astra proposed the proofs and generated the Lean formalization, and that GPT-5.6 Sol and Claude Opus 5 did editorial review. The README of the Lean archive says, separately, that the Lean code was generated with OpenAI Codex (GPT-6).

Submission note. Posted to erdosproblems.com as a proof claim by Qiyuan Gu (account fireflysentinel) on 8 September 2026, giving "GPT-6 Astra" as the AI used:

We prove that an additive function f : ℕ → ℝ with #{n ≤ X : f(n+1) < f(n)} = o(X) must satisfy f(n) = c log n for some c ≥ 0. Assuming finite concentration fails, we normalize and clip f, obtaining a strongly additive approximation with positive variance from the Ruzsa–Hildebrand moment estimates. The density-zero decrease condition and Mangerel’s short-interval theorem force the same variance to vanish, giving a contradiction. Notes: GPT-6 Astra was used to generate the mathematical proofs and draft the manuscript. The author reviewed the final manuscript and takes full responsibility for its content.

Argument, as the manuscript states it. The step to prove is finite concentration: for some $d>0$ and $R<\infty$, and arbitrarily large $X$, some interval of length $R$ holds at least $dX$ of the values $f(n)$, $n\le X$. By Erdős's Theorem V of 1946 this is equivalent to the convergence of $\sum_p\min\{(f(p)-c\log p)^2,1\}/p$ for some $c$, and under that convergence Hildebrand's limiting law for $f(n+1)-f(n)$ together with the density hypothesis forces $f=c\log$. Assuming finite concentration fails, the manuscript normalizes $f$ modulo a logarithmic term and clips it, so that Ruzsa's second-moment estimate gives the clipped function a positive variance, while the density-zero decrease condition, Mangerel's short-interval first-moment theorem (Theorem 1.1 of Mangerel 2022) and Elliott's fourth-moment inequality bound the same variance from above by a quantity that tends to zero, a contradiction. The known results it extends are Erdős's theorem for an empty set of decreases or for $f(n+1)-f(n)\to0$, Hildebrand's density-one version, and Mangerel's Corollary 1.7, which gives the conclusion for completely additive $f$ under a stronger sparseness bound on the decreases and a condition on the prime values.

Lean development. The archive in the Zenodo record (the files of the 2026-09-23 revision, which the formalization link's date records) proves Erdos1122.Statements.main_of_cited : Mangerel → Ruzsa → ErdosV → Hildebrand → ErdosProblem1122, where ErdosProblem1122 states the claim above with the decreases counted over $0<n\le\lfloor X\rfloor$ and the four premises are propositions encoding the cited results of Mangerel, Ruzsa, Erdős and Hildebrand; its Check.lean guards the theorem's axioms to propext, Classical.choice and Quot.sound. The development is therefore a checked derivation of the claim from four unformalized theorems, and its README says that the correspondence between the Lean premises and the source statements remains for human review. The corpus has not built, replayed or audited the development, so the link is recorded as a posting of the result, not as formalized evidence.

Depends on. No page of this wiki.

Acceptance. None recorded. The site's label is OPEN (problem page last edited 2026-04-01); the proof-claims entry carries no comments and no acceptance mark, and no review, referee report or acknowledgment by anyone outside the claimant is on record. The argument is not compiled in this wiki.