Skip to content

Erdős problem 321

Start work

What is the largest A⊆{1,…,N}A\subseteq\{1,\dots,N\} such that all subset sums ∑n∈S1/n\sum_{n\in S}1/n (over S⊆AS\subseteq A) are distinct?

Open in the state represented here.

At Formal Conjectures commit 59f30aa314ba225fcd9268723ce8291616df1ab0, the Lean development starfleet/erdos-321 establishes a two-sided asymptotic bound on extremalSize, which denotes the same quantity as Formal Conjectures' Erdos321.R and therefore supplies a candidate answer for the exact occurrence Erdos321.erdos_321.variants.isTheta, not a proof of it.

How far the record reaches6 of 6 stages
  1. Sourceerdos-problems
  2. StatementRetained
  3. Formal6 retained
  4. Resolutionsolved
  5. Work1 check
  6. Decisionaccepted
  7. The questionNot reached
The accepted scope sits inside the question, and does not reach it.
Scope of what is proved
The question aboveNot established here
Proved and acceptedaccepted

A two-sided asymptotic bound on extremalSize

Results1
A two-sided asymptotic bound on extremalSize
Aug 17, 2026, 6:33 PM · 1 evidence item · replaces an earlier Result · current
accepted
Checks1 scoped
Claim chain fidelity
Does not establish: A proof, resolution, statement equivalence, fresh kernel execution, independent reproduction, acceptance, or Standing.
pass
A check reports only its own scope. The Decision accepted the Claim, not the check.
Inspect evidenceReproduce checksStart work