Skip to content

Erdős problem 443

Start work

Let m,n≥1m,n\geq 1. What is #{k(m−k):1≤k≤m/2}∩{l(n−l):1≤l≤n/2}?\# \{ k(m-k) : 1\leq k\leq m/2\} \cap \{ l(n-l) : 1\leq l\leq n/2\}? Is it ≤(mn)o(1)\leq (mn)^{o(1)} for all sufficiently large m,nm,n?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/443.lean

Formal Conjectures

FormalConjectures/ErdosProblems/443.leanErdos443.erdos_443.parts.i1 lineExact file
True ↔ ∀ (s : ℕ), ∃ m, ∃ n < m, s ≤ (Erdos443.A n ∩ Erdos443.A m).card
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:443
  • PLBY Lean proofsErdosProblems.Erdos443

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry