Erdős Problem 888

Reference: erdosproblems.com/888

def Erdos888.RequiredCondition (A : Finset ℕ) (n : ℕ) : Prop

Condition on the sets A appearing in Erdős 888. Namely, let A be a subset of {1,...,n} such that if a ≤ b ≤ c ≤ d ∈ A and abcd square then ad=bc.

Equations

• Erdos888.RequiredCondition A n = (A ⊆ Finset.Ioc 0 n ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≤ b → b ≤ c → c ≤ d → IsSquare (a * b * c * d) → a * d = b * c)

def Erdos888.p (n k : ℕ) : Prop

Proposition that for a specific n an A with the above defined condition and cardinality k exists.

Equations

• Erdos888.p n k = ∃ (A : Finset ℕ), Erdos888.RequiredCondition A n ∧ A.card = k

theorem Erdos888.erdos_888 (n : ℕ) : Nat.findGreatest (p n) n = sorry n

What is the size of the largest subset A of {1,...,n} such that if a ≤ b ≤ c ≤ d ∈ A and abcd square then ad=bc

theorem Erdos888.erdos_888_Sárközy : (fun (n : ℕ) => ↑(Nat.findGreatest (p n) n)) =o[Filter.atTop] Nat.cast

|A|=o(n).

theorem Erdos888.erdos_888_primes : (fun (n : ℕ) => ↑n / Real.log ↑n) =O[Filter.atTop] fun (n : ℕ) => ↑(Nat.findGreatest (p n) n)

The primes show that |A| ≫ n/log n is possible.