Skip to content

Erdős problem 888

Start work

What is the size of the largest A⊆{1,…,n}A\subseteq \{1,\ldots,n\} such that if a≤b≤c≤d∈Aa\leq b\leq c\leq d\in A are such that abcdabcd is a square then ad=bcad=bc?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

888.lean

Retained formal statement1 of 4

What is the size of the largest A⊆{1,…,n}A\subseteq \{1,\ldots,n\} such that if a≤b≤c≤d∈Aa\leq b\leq c\leq d\in A are such that abcdabcd is a square then ad=bcad=bc?

This was proved by GPT-5.5 Pro (prompted by Chojecki).

FormalConjectures/ErdosProblems/888.leanErdos888.erdos_8881 lineExact file
(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n
SolvedStatement only, no proof