Erdős’s 1946 conjecture on almost-monotone additive functions (Erdős problem #1122) proved in an anonymous Zenodo preprint whose proofs and Lean code were generated by GPT-6 Astra; Mangerel builds on it to settle Sárközy’s 2001 conjectures
Awaiting review
The takeaway
On Sept 7, 2026 an anonymous author posted “Almost everywhere monotone additive functions” on Zenodo.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 10 October 2026
Your AI and this story
- GPT-6 Astra130 days after its cutoff
- Claude Opus 5.569 days after its cutoff
- Gemini 3.8 Flash160 days after its cutoff
- Grok 4.799 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 69 days before it.
Key facts
- Problem (Erdős 1946, Ann. of Math. 47; erdosproblems.com #1122): if f is additive and #{n ≤ X : f(n+1) < f(n)} = o(X), must f(n) = c log n? Erdős proved it when f never decreases or when f(n+1) − f(n) → 0
- Earlier partial progress: Mangerel (arXiv 2108.12351, published 2022) proved it when the decreases number ≪ X/(log X)^(2+c) and f(p) is not too large
- Preprint: Anonymous, ‘Almost everywhere monotone additive functions’, Zenodo 10.5281/zenodo.22651918 (v1 Sept 7, 2026; v2 Sept 22 adds erdos-1122-lean.zip). About 64 views and 32 downloads by Oct 10
- Method (abstract): deduce finite concentration without a growth assumption on higher prime powers, via a truncated normalization and bounded clipping that reduce to Mangerel’s first-moment short-interval theorem, Ruzsa’s second-moment estimate and Elliott’s fourth-moment inequality
- AI disclosure: ‘GPT-6 Astra was used to propose the mathematical proofs and generate the Lean formalization. GPT-5.6 Sol and Claude Opus 5 were used for editorial review of the exposition. The author finished the final manuscript and takes full responsibility for its content.’
- Lean 4: the formalization treats the cited results of Mangerel, Ruzsa, Erdős and Hildebrand as hypotheses, so it is not a full formal proof from Mathlib. We have not compiled it
- Oct 6, 2026: Alexander P. Mangerel, ‘On Sárközy’s Local Extrema Conjectures’ (arXiv 2610.08424): ‘Recently, an AI-assisted proof of problem (ii’) was obtained [1] that relied crucially on this work’. He says his paper is ‘inspired by the method in [1]’ and that the AI paper does not adequately describe its context. He resolves, in a strong form, Sárközy’s two 2001 conjectures on multiplicative functions with finitely many local maxima or minima
- erdosproblems.com/1122 (checked Oct 10): one proof claim listed, but the page was last edited April 1, 2026 and the problem is not yet marked solved. New proof claims there were suspended in early October
What happened
In 1946 Erdős proved that an additive function (f(ab) = f(a) + f(b) for coprime a, b) that never decreases must be a constant multiple of log n. He conjectured that the same holds if it decreases only on a set of natural density zero. The question is listed as problem #1122 on Thomas Bloom’s erdosproblems.com. Alexander Mangerel made the best partial progress (2021–22).
On Sept 7, 2026 an anonymous author posted an 8-page proof on Zenodo, tagged “Erdős Problem 1122”. A second version on Sept 22 added a Lean 4 project. The paper’s “Declaration of generative AI use” says OpenAI’s GPT-6 Astra proposed the proofs and generated the Lean formalization. The record drew little attention (about 60 views by Oct 10).
It surfaced on Oct 6, when Mangerel posted “On Sárközy’s Local Extrema Conjectures” on arXiv. He cites the Zenodo paper as “an AI-assisted proof” of Erdős’s conjecture that “relied crucially” on his earlier work. He describes its two-step strategy (finite concentration, then rigidity), says his own paper is inspired by it, and uses the method to classify all positive multiplicative functions with rare local maxima or minima. This settles two 2001 conjectures of András Sárközy in strong form. Mangerel’s paper itself has no AI-use statement that we found.
We found this through the Oct 10 arXiv sweep. It flagged Mangerel’s paper only as “claiming to settle conjectures”, because the AI mention sits in his introduction, not in a disclosure section. We found no press or social-media discussion.
Why it matters
It fits the autumn 2026 pattern of Erdős problems and old conjectures settled by frontier models and posted outside arXiv, anonymously or by unknown authors. It is also an early case of a specialist openly building new human research on an AI-generated proof. The proof has not been peer-reviewed, and the Lean code assumes the cited analytic theorems as hypotheses.
What is disputed or not yet verified
| Verification | Preprint on Zenodo with a Lean 4 formalization that assumes cited results as hypotheses; used by a specialist (Mangerel) in follow-up work; not peer-reviewed; not marked solved on erdosproblems.com |
|---|
Sources
4 sources from 3 sites. Numbers match the chips in the text.
4 sources: 3 primary, 1 reaction
Primary
- Zenodo: Almost everywhere monotone additive functions (Anonymous, Erdős Problem 1122)doi.org, paper
- arXiv 2610.08424: A. P. Mangerel, On Sárközy’s Local Extrema Conjecturesarxiv.org, paper
- arXiv 2108.12351: A. P. Mangerel, Additive functions in short intervals, gaps and a conjecture of Erdősarxiv.org, paper
Reactions
- Erdős Problem #1122 (T. F. Bloom, erdosproblems.com)erdosproblems.com, discussion
Changes
- Filed from the Oct 10 arXiv sweep (Mangerel 2610.08424 → Zenodo record)