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

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.

FormalConjectures/ErdosProblems/125.leanErdos125.erdos_1251 lineExact file
False ↔ ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity
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.