Skip to content

Erdős problem 844

Let A⊆{1,…,N}A\subseteq \{1,\ldots,N\} be such that, for all a,b∈Aa,b\in A, the product abab is not squarefree.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/844.lean

Formal Conjectures

FormalConjectures/ErdosProblems/844.leanErdos844.erdos_8444 linesExact file
True ↔  ∀ (N : ℕ),    IsGreatest {k | ∃ A ⊆ Finset.Icc 1 N, (∀ a ∈ A, ∀ b ∈ A, ¬Squarefree (a * b)) ∧ A.card = k}      (Erdos844.evenOrOddNonSquarefree N).card
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:844
  • PLBY Lean proofsErdosProblems.Erdos844

Reported activity

Reported by these sources. Not reviewed here.

Continue