542.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 8 contain sorry, 0 declared as axioms

Erdős Problem 542

References:

erdosproblems.com/542
[Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
[Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180.
[ScSz59] Schinzel, A. and Szekeres, G., Sur un problème de M. Paul Erdős. Acta Sci. Math. (Szeged) (1959), 221-229.
[Ch96] Chen, Yong-Gao, On a problem of P. Erdős. Acta Sci. Math. (Szeged) (1996), 101--114.

Imports (1)

FormalConjecturesUtil

def Erdos542.IsLcmFree A set A ⊆ {1, …, n} such that lcm(a, b) > n for all distinct a, b ∈ A line 44 source
Source documentation
A set A ⊆ {1, …, n} such that lcm(a, b) > n for all distinct a, b ∈ A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: And, LE.le, Finset.Icc, OfNat.ofNat, Set.Pairwise, LT.lt, Nat.lcm
9 instances, coercions and auxiliary constants left out.
```
def IsLcmFree (n : ℕ) (A : Finset ℕ) : Prop :=
…
```
def Erdos542.uncovered The integers 1 ≤ m ≤ n which are not divisible by any element of A line 48 source
Source documentation
The integers 1 ≤ m ≤ n which are not divisible by any element of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, Membership.mem, Not, Dvd.dvd, Finset.Icc, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
```
def uncovered (n : ℕ) (A : Finset ℕ) : Finset ℕ :=
…
```
theorem Erdos542.erdos_542.parts.i sorry line 61 source
depends on sorry what this means
Statement uses: Iff, True, Nat, Finset, Erdos542.IsLcmFree, LE.le, Real, Finset.sum, HDiv.hDiv, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos542.erdos_542.variants.sharp sorry line 68 source
depends on sorry what this means
Statement uses: And, Erdos542.IsLcmFree, OfNat.ofNat, Nat, Insert.insert, Finset, Singleton.singleton, Eq, Real, Finset.sum, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos542.erdos_542.parts.ii sorry line 83 source
depends on sorry what this means
Statement uses: Iff, False, Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Finset, Erdos542.IsLcmFree, Not, Membership.mem, LE.le, HMul.hMul, Finset.card, Erdos542.uncovered
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos542.erdos_542.variants.schinzel_szekeres sorry line 95 source
depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, Nat, Finset, And, Erdos542.IsLcmFree, Not, Membership.mem, LE.le, Finset.card, Erdos542.uncovered, HMul.hMul, LT.lt, HSub.hSub, Finset.sum, HDiv.hDiv
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos542.erdos_542.variants.log_power Schinzel and Szekeres [ScSz59] proved that there are examples $A\subseteq\{2,\ldots,n\}$ with at most $n/(\log n)^c$ many such $m$, for some real constant $c>0$ sorry line 105 source
Source documentation
Schinzel and Szekeres [ScSz59] proved that there are examples $A\subseteq\{2,\ldots,n\}$ with at most $n/(\log n)^c$ many such $m$, for some real constant $c>0$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Frequently, Nat, Finset, Erdos542.IsLcmFree, Not, Membership.mem, LE.le, Finset.card, Erdos542.uncovered, HDiv.hDiv, HPow.hPow, Real.log, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_542.variants.log_power : ∃ c > (0 : ℝ), ∃ᶠ n : ℕ in atTop, ∃ A : Finset ℕ,
    IsLcmFree n A ∧ 1 ∉ A ∧ ((uncovered n A).card : ℝ) ≤ n / (log n) ^ c := by
…
```
Mentions: c, Erdos542.IsLcmFree, Erdos542.uncovered
theorem Erdos542.erdos_542.variants.chen Chen [Ch96] has proved that if $n>172509$ then $$\sum_{a\in A}\frac{1}{a}< \frac{1}{3}+\frac{1}{4}+\frac{1}{5}+\frac{1}{7}+\frac{1}{11}.$$ sorry line 114 source
Source documentation
Chen [Ch96] has proved that if $n>172509$ then $$\sum_{a\in A}\frac{1}{a}< \frac{1}{3}+\frac{1}{4}+\frac{1}{5}+\frac{1}{7}+\frac{1}{11}.$$

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Erdos542.IsLcmFree, Real, Finset.sum, HDiv.hDiv, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_542.variants.chen (n : ℕ) (hn : 172509 < n) (A : Finset ℕ) (hA : IsLcmFree n A) :
    ∑ a ∈ A, (1 : ℝ) / a < 1 / 3 + 1 / 4 + 1 / 5 + 1 / 7 + 1 / 11 := by
…
```
Mentions: Erdos542.IsLcmFree
theorem Erdos542.erdos_542.variants.one_add_little_o In [Er73] Erdős further speculates that in fact $$\sum_{a\in A}\frac{1}{a}\leq 1+o(1),$$ where the $o(1)$ term $\to 0$ as $n\to \infty$ sorry line 124 source
Source documentation
In [Er73] Erdős further speculates that in fact $$\sum_{a\in A}\frac{1}{a}\leq 1+o(1),$$ where the $o(1)$ term $\to 0$ as $n\to \infty$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, Finset, Erdos542.IsLcmFree, LE.le, Finset.sum, HDiv.hDiv, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_542.variants.one_add_little_o : answer(sorry) ↔
    ∃ o : ℕ → ℝ, Tendsto o atTop (nhds 0) ∧
      ∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → ∑ a ∈ A, (1 : ℝ) / a ≤ 1 + o n := by
…
```
Mentions: Erdos542.IsLcmFree
theorem Erdos542.erdos_542.variants.only_two In [Er98] Erdős mentions that he, Schinzel, and Szekeres conjectured that $2,3,5$ and $3,4,5,7,11$ are the only two sequences for which the sum is $>1$ sorry line 134 source
Source documentation
In [Er98] Erdős mentions that he, Schinzel, and Szekeres conjectured that $2,3,5$ and $3,4,5,7,11$ are the only two sequences for which the sum is $>1$.

depends on sorry what this means
Statement uses: Iff, True, Nat, Finset, Erdos542.IsLcmFree, LT.lt, Real, OfNat.ofNat, Finset.sum, HDiv.hDiv, Or, Eq, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_542.variants.only_two : answer(sorry) ↔
    ∀ (n : ℕ) (A : Finset ℕ), IsLcmFree n A → 1 < ∑ a ∈ A, (1 : ℝ) / a →
      A = {2, 3, 5} ∨ A = {3, 4, 5, 7, 11} := by
…
```
Mentions: Erdos542.IsLcmFree