Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Let $f_3(N)$ be the least size forcing a set $A \subseteq \{1,\ldots,N\}$ to contain distinct $a,b,c$ with $a+b$, $a+c$ and $b+c$ all in $A$. The upper bound $f_3(N) \le 5N/8 + O(1)$ matches the standard construction $[N/8,N/4] \cup [N/2,N]$, so $f_3(N) = 5N/8 + O(1)$.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
The paper states that the manuscript was written by GPT-5.5 Pro from a proof developed by the author together with GPT-5.5 Pro, and that the accompanying Lean formalization was carried out with Aristotle. Both the mathematics and the write-up are joint with the model rather than checked by it.
Provider: OpenAI / Harmonic · Prompt public: unknown · Independence: unknown
The paper reports a Lean formalization against Mathlib with no sorries and no added axioms. We have not compiled it. arXiv preprint, not peer-reviewed.
Correctness: supported · statement fidelity: audited · peer review: none
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.