Erdős problem 125 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

125.lean

Retained formal statement3 of 6

Case 4: Does $A + 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

1False ↔2  0 < ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity ∧3    ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).lowerDensity <4      ({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.

Sources

Search problems.science