erdős #535
Let , and let denote the size of the largest subset of such that no subset of size has the same pairwise greatest common divisor between all elements. Estimate .
Open — best to date is a partial proof, not yet sealed.
number theory · open · possible · formalized (Lean) · 1 attempt
machinery: sunflower-conjecture-erdos-rado,prime-power-layer-encoding,smooth-rough-decomposition,Rankin-smooth-number-bound,Omega-prime-factor-multiplicity,constant-pairwise-gcd-system,extremal-set-system
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
partial proof
needs verification
Erdos 535 remains open; I give a rigorous conditional reduction (strong Omega-sunflower bound g_r(k)<=c_r^k => f_r(N)<=N^{2 ln c_r/loglog N}), with the layer/Poisson counting mechanism proven analytic
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Write (A\subseteq{1,\dots,N}). A set of $r$ distinct integers ({a_1,\dots,a_r}\subset A) has **all pairwise gcd’s equal** iff there is some (d\ge1) such that [ \gcd(a_i,a_j)=d\quad(\forall i\ne j). ] Equivalently, [ a_i=d,b_i\quad\text{and}\quad \gcd(b_i,b_j)=1\ \ (\forall i\ne j), ] i.e. after factoring out the common…
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 11 · open (literature)
theorem erdos_535 : ∀ r ≥ 3, ∃ c > (0 : ℝ),
∀ᶠ (N : ℕ) in atTop,
(f r N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ)))formal-conjectures/535.lean ↗status
open