Skip to content

Erdős problem 125

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 statement3 of 6

Case 4: Does A+BA + B have positive upper and lower density that are unequal?

This follows from the disproof erdos_125.variants.positive_lower_density above.

FormalConjectures/ErdosProblems/125.leanErdos125.erdos_125.variants.positive_unequal_density4 linesExact file
False ↔  0 < ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity ∧    ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity <      ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).upperDensity
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.