Skip to content

Erdős problem 862

Let A1(N)A_1(N) be the number of maximal Sidon subsets of {1,,N}\{1,\ldots,N\}. Is it true that A1(N)>2NcA_1(N) > 2^{N^c} for some constant c>0c>0?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/862.lean

Formal Conjectures

FormalConjectures/ErdosProblems/862.leanErdos862.erdos_862.parts.i1 lineExact file
False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:862
  • PLBY Lean proofsErdosProblems.Erdos862

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page