Erdős problem 677
Denote by the least common multiple of the finite set . Is it true that for all , we get ?
Sources
FormalConjectures/ErdosProblems/
677.lean
Retained formal statement
Erdős expected very few solutions for , where and . The only solutions he knew were the following.
Finset.lcmInterval 4 3 = Finset.lcmInterval 13 2 ∧ Finset.lcmInterval 3 4 = Finset.lcmInterval 19 2TestStatement only, no proof