Erdős problem 100

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

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.