Skip to content

Erdős problem 125

Start work

Case 3: Does A+BA + B have positive upper and lower density that are equal? This is the literal interpretation of "positive density" which was falsified.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

125.lean

Retained formal statement2 of 6

Literature question: Does A+BA + B have positive lower density?

This has been falsified.

FormalConjectures/ErdosProblems/125.leanErdos125.erdos_125.variants.positive_lower_density1 lineExact file
False ↔ 0 < ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.