erdős #319

← #318 · #320 → (packet.json; erdosproblems.com)

What is the size of the largest $A \subseteq {1, \dots, N}$ such that there is a function $δ : A \to {- 1, 1}$ such that $n \in A \sum \frac{δ _{n}}{n} = 0$ and $n \in A^{'} \sum \frac{δ _{n}}{n} \neq = 0$ for all non-empty $A^{'} ⊊ A$ ?

Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.

number theory · open · possible · formalized (Lean) · 4 attempts

machinery: unit-fractions,egyptian-fractions,short-interval-unit-fraction-representation,croot-dense-denominators,signed-zero-sum-minimality,subset-sum-vanishing-constraint,density-of-extremal-set,prime-distribution

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

routes

formal prooflean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

verified computationpython:verify_319_smoothness_counting.py

N-smoothness upper-bound counting corroboration (pinned tier: scripts/requirements-verifiers.txt)

obstruction reportreview

precise, artifact-backed reason a route cannot work

banked

the counting step of the upper bound corroborated numerically

targets

the full upper bound is not established by the numerics alone.1

evidence

partial proof

needs verification

The asymptotic-order variants of Erdős #319 (isTheta/isBigO/isLittleO) are settled: c(N)=Θ(N) with gauge g(N)=N, immediately from the trivial bound c(N)≤N plus the already-accepted Croot/Adenwalla lower bound c(N)≥(1−1/e+o(1))N. The only genuinely open content is the exact constant κ=lim c(N)/N ∈ [1−1/e,1] (conjecturally 1; the natural p-adic obstruction is only o(N), so it does not force κ<1) and the finite IsGreatest values. Exact small values verified: c(6)=4 ({1,2,3,6}), c(12)=6 ({1,2,3,4,6,12}).

partial proof

machine-sealed

Erdos #319: a meet-in-the-middle exhaustive enumeration verifies the exact finite table through N=27: c(N)=0 for 1<=N<=5, 4 for 6<=N<=11, 6 for 12<=N<=14, 8 for 15<=N<=17, 10 for 18<=N<=20, 12 for 21<=N<=23, and 14 for 24<=N<=27. This finite table does not address the official all-N extremal question.

{"scope":{"target":"#319 exact finite table extension","max_N":27,"method":"Meet-in-the-middle exhaustive enumeration of signed subsets of {1,...,N}, clearing denominators by lcm(1,...,N).","does_n...

[{"method":"independent_script","command":"python3 scripts/verify_erdos319_mitm_table.py examples/erdos-problems/attack/erdos319-mitm-exact-table-record-draft.v1.json","result":"passed"}]

partial proof

machine-sealed

Erdos #319: lean/Vela/Erdos319Smoothness.lean kernel-verifies the smoothness mechanism behind the upper bound. For a signed-zero set A and a prime p, if the isolation bound |T| < p holds (T the cleared A_p numerator), then the p-divisible part A_p is itself signed-zero; hence by irreducibility A_p = A, so every element of an extremal irreducible set is (N/m)-smooth with m = floor((1/2) ln N). Combined with the prime-number-theorem count of non-(N/m)-smooth integers (numerically corroborated) this gives c(N) <= N - (1+o(1)) N loglog N / log N. With the known (1-1/e)N lower bound (Croot 2001 / Martin 2000 / Adenwalla) this yields Theta(c(N)) = Theta(N); the sharp leading constant is not determined here.

{"lean_file":"lean/Vela/Erdos319Smoothness.lean","lean_theorems":["Ap_signed_zero: signed-zero A + prime p + |T|<p -> sgnSum (Ap A p) = 0","Ap_eq_self_of_irreducible: irreducible A + nonempty A_p...

depends on (the wall): lean/Vela/Erdos319Smoothness.lean; scripts/verify_319_smoothness_counting.py

lake build Vela.Erdos319Smoothness (sorry/axiom-clean) + scripts/verify_319_smoothness_counting.py

partial proof

machine-sealed

Erdos #319: every irreducible signed-zero set A subset {1..N} has bounded harmonic mass, sum_{a in A} 1/a <= 2 (log N)^{4/5+o(1)}. Proof: if a side's reciprocal mass exceeds the Liu-Sawhney (IMRN 2026) threshold (log N)^{4/5+o(1)}, that side contains a subcollection of reciprocal sum 1; if the common side-sum S>1 the two unit-subcollections form a nonempty proper signed-zero subset, contradicting irreducibility. This is a proven structural property; it does not determine the sharp constant of c(N) (it is too weak to push the cardinality bound below N - o(N)).

{"result":"irreducible => sum_{a in A} 1/a <= 2 (log N)^{4/5+o(1)}","exact_irreducibility_criterion":"Sigma(P) cap Sigma(Q) = {0,S} (subset-sum reciprocal spectra of the two sides meet only trivial...

depends on (the wall): lean/Vela/Erdos319Smoothness.lean

Liu-Sawhney IMRN 2026 (Crossref-verified) + derivation review

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

[ M(N):=\max\\{|A|:\ A\subseteq{1,\dots,N}\ \text{and}\ \exists,\delta:A\to{\pm1}\ \text{with}\ \sum_{n\in A}\frac{\delta_n}{n}=0, \ \sum_{n\in A'}\frac{\delta_n}{n}\neq 0\ \forall,\varnothing\neq A'\subsetneq A\\}. ]

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_319 (N : ℕ) : IsGreatest
    { #A | (A) (_ : A ⊆ Finset.Icc 1 N)
      (_ : ∃ δ : ℕ → ℤˣ, ∑ n ∈ A, (δ n : ℚ) / n = 0 ∧
        ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', (δ n : ℚ) / n ≠ 0) }
    answer(sorry)

formal-conjectures/319.lean ↗

Vela formalization: Erdos319Smoothness.lean (sorry-free), Erdos319.lean (sorry-free)

links

Google DeepMind Formal Conjectures project · link

status

open

routes

banked

targets

evidence

formal

links

status

Search Vela