Erdős problem 536

Let

\epsilon>0

and

N

be sufficiently large. Is it true that if

A\subseteq \{1,\ldots,N\}

has size at least

\epsilon N

then there must be distinct

a,b,c\in A

such that

[a, b]=[b, c]=[a, c],

where

[\cdot, \cdot]

denotes the least common multiple?

Withdrawn 19 Aug 2026

WITHDRAWN (removed from the active solver pool by maintainer request)

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«536»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos536.erdos_536" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ ε > 0,
    ∀ᶠ (N : ℕ) in Filter.atTop,
      ∀ A ⊆ Finset.Icc 1 N,
        ε * ↑N ≤ ↑A.card → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, {a, b, c}.card = 3 ∧ a.lcm b = b.lcm c ∧ b.lcm c = a.lcm c

Original conjecture source: FormalConjectures/ErdosProblems/536.lean

Task id: fc-379fc029-erdos536-erdos-536-3571e2d944-formalized-v1
Task commitment: sha256:b33ae3944c41d5a0b9ee4c717e76703e6b1c3d471dfb10721ab129ba54979abb

References

erdosproblems.com/536

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1 →