Erdős problem 321
What is the largest such that all subset sums (over ) are distinct?
- Formal statements
- 4 open · 2 solved
- Erdős Problems says
- solved
- Decision here
- accepted
- Checks
- 1 check · 6 formal
A two-sided asymptotic bound on extremalSize
Still unresolved: 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.
Exact result and limitations
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. For occurrence resolution only, the exact occurrences Erdos321.erdos_321 and Erdos321.erdos_321.variants.isTheta are associated with problem:erdos:321 under resolver root sha256:a9d6787719c5c8069a9e14ade0f5a62975410272e6cd1583865b282d1d8669dd. At the exact retained Erdős 321 source revisions, the terminal theorem and structural comparison do not establish implication to either fixed Nat.log variant.
- Exact source revisions, occurrence resolver root, and retained evidence/current/erdos-321 inputs only.
- Caveat: Erdos problem 321 remains open; this does not assert resolution or optimality.
- Caveat: Occurrence association is navigation-only and establishes no statement equivalence.
- Caveat: The negative comparison does not show that a bridge is impossible or that either statement is false.
- Caveat: The retained terminal and fixed sources have no exact resolved joint Lean environment.
- Type
- theoretical
- Evidence
- 1 artifact
- Decision
- accepted
- Reviewed
- Aug 17, 2026, 6:33 PM