Erdős problem 100 · problems.science

From [Piepmeyer]: 9 points with diameter $< 5$ . TODO: find reference

Sources

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

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

100.lean

Retained formal statement2 of 5

From [Piepmeyer]: 9 points with diameter $< 5$ . TODO: find reference

FormalConjectures/ErdosProblems/100.leanErdos100.erdos_100_piepmeyer1 lineExact file

1∃ A, A.card = 9 ∧ Erdos100.DistancesSeparated A ∧ Metric.diam ↑A < 5

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.